Theory Global_Invariants_Lemmas

(*<*)
(*
 * Copyright 2015, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

theory Global_Invariants_Lemmas
imports
  Global_Invariants
begin

declare subst_all [simp del] [[simproc del: defined_all]]

(*>*)
section‹Global invariants lemma bucket›

(* FIXME this file should be about the invs. This split makes it easier to move things around, maybe. *)

declare mut_m.mutator_phase_inv_aux.simps[simp]
case_of_simps mutator_phase_inv_aux_case: mut_m.mutator_phase_inv_aux.simps
case_of_simps sys_phase_inv_aux_case: sys_phase_inv_aux.simps


subsection‹TSO invariants›

lemma tso_store_inv_eq_imp:
  "eq_imp (λp s. mem_store_buffers (s sys) p)
          tso_store_inv"
by (simp add: eq_imp_def tso_store_inv_def)

lemmas tso_store_inv_fun_upd[simp] = eq_imp_fun_upd[OF tso_store_inv_eq_imp, simplified eq_imp_simps, rule_format]

lemma tso_store_invD[simp]:
  "tso_store_inv s ⟹ ¬sys_mem_store_buffers gc s = mw_Mutate r f r' # ws"
  "tso_store_inv s ⟹ ¬sys_mem_store_buffers gc s = mw_Mutate_Payload r f pl # ws"
  "tso_store_inv s ⟹ ¬sys_mem_store_buffers (mutator m) s = mw_fA fl # ws"
  "tso_store_inv s ⟹ ¬sys_mem_store_buffers (mutator m) s = mw_fM fl # ws"
  "tso_store_inv s ⟹ ¬sys_mem_store_buffers (mutator m) s = mw_Phase ph # ws"
by (auto simp: tso_store_inv_def dest!: spec[where x=m])

lemma mut_do_store_action[simp]:
  "⟦ sys_mem_store_buffers (mutator m) s = w # ws; tso_store_inv s ⟧ ⟹ fA (do_store_action w (s sys)) = sys_fA s"
  "⟦ sys_mem_store_buffers (mutator m) s = w # ws; tso_store_inv s ⟧ ⟹ fM (do_store_action w (s sys)) = sys_fM s"
  "⟦ sys_mem_store_buffers (mutator m) s = w # ws; tso_store_inv s ⟧ ⟹ phase (do_store_action w (s sys)) = sys_phase s"
by (auto simp: do_store_action_def split: mem_store_action.splits)

lemma tso_store_inv_sys_load_Mut[simp]:
  assumes "tso_store_inv s"
  assumes "(ract, v) ∈ { (mr_fM, mv_Mark (Some (sys_fM s))), (mr_fA, mv_Mark (Some (sys_fA s))), (mr_Phase, mv_Phase (sys_phase s)) }"
  shows "sys_load (mutator m) ract (s sys) = v"
using assms
apply (clarsimp simp: sys_load_def fold_stores_def)
apply (rule fold_invariant[where P="λfr. do_load_action ract (fr (s sys)) = v" and Q="mut_writes"])
  apply (fastforce simp: tso_store_inv_def)
 apply (auto simp: do_load_action_def split: mem_store_action.splits)
done

lemma tso_store_inv_sys_load_GC[simp]:
  assumes "tso_store_inv s"
  shows "sys_load gc (mr_Ref r f) (s sys) = mv_Ref (Option.bind (sys_heap s r) (λobj. obj_fields obj f))" (is "?lhs = mv_Ref ?rhs")
using assms unfolding sys_load_def fold_stores_def
apply clarsimp
apply (rule fold_invariant[where P="λfr. Option.bind (heap (fr (s sys)) r) (λobj. obj_fields obj f) = ?rhs"
                             and Q="λw. ∀r f r'. w ≠ mw_Mutate r f r'"])
  apply (fastforce simp: tso_store_inv_def)
 apply (auto simp: do_store_action_def map_option_case fun_upd_apply
            split: mem_store_action.splits option.splits)
done

lemma tso_no_pending_marksD[simp]:
  assumes "tso_pending_mark p s = []"
  shows "sys_load p (mr_Mark r) (s sys) = mv_Mark (map_option obj_mark (sys_heap s r))"
using assms unfolding sys_load_def fold_stores_def
apply clarsimp
apply (rule fold_invariant[where P="λfr. map_option obj_mark (heap (fr (s sys)) r) = map_option obj_mark (sys_heap s r)"
                             and Q="λw. ∀fl. w ≠ mw_Mark r fl"])
  apply (auto simp: map_option_case do_store_action_def filter_empty_conv fun_upd_apply
             split: mem_store_action.splits option.splits)
done

lemma no_pending_phase_sys_load[simp]:
  assumes "tso_pending_phase p s = []"
  shows "sys_load p mr_Phase (s sys) = mv_Phase (sys_phase s)"
using assms
apply (clarsimp simp: sys_load_def fold_stores_def)
apply (rule fold_invariant[where P="λfr. phase (fr (s sys)) = sys_phase s" and Q="λw. ∀ph. w ≠ mw_Phase ph"])
  apply (auto simp: do_store_action_def filter_empty_conv
             split: mem_store_action.splits)
done

lemma gc_no_pending_fM_write[simp]:
  assumes "tso_pending_fM gc s = []"
  shows "sys_load gc mr_fM (s sys) = mv_Mark (Some (sys_fM s))"
using assms
apply (clarsimp simp: sys_load_def fold_stores_def)
apply (rule fold_invariant[where P="λfr. fM (fr (s sys)) = sys_fM s" and Q="λw. ∀fl. w ≠ mw_fM fl"])
  apply (auto simp: do_store_action_def filter_empty_conv
             split: mem_store_action.splits)
done

lemma tso_store_refs_simps[simp]:
  "mut_m.tso_store_refs m (s(mutator m' := s (mutator m')⦇roots := roots'⦈))
 = mut_m.tso_store_refs m s"
  "mut_m.tso_store_refs m (s(mutator m' := s (mutator m')⦇ghost_honorary_root := {}⦈,
                             sys := s sys⦇mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := sys_mem_store_buffers (mutator m') s @ [mw_Mutate r f opt_r'])⦈))
 = mut_m.tso_store_refs m s ∪ (if m' = m then store_refs (mw_Mutate r f opt_r') else {})"
  "mut_m.tso_store_refs m (s(sys := s sys⦇mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := sys_mem_store_buffers (mutator m') s @ [mw_Mutate_Payload r f pl])⦈))
 = mut_m.tso_store_refs m s ∪ (if m' = m then store_refs (mw_Mutate_Payload r f pl) else {})"
  "mut_m.tso_store_refs m (s(sys := s sys⦇heap := (sys_heap s)(r' := None)⦈))
 = mut_m.tso_store_refs m s"
  "mut_m.tso_store_refs m (s(mutator m' := s (mutator m')⦇roots := insert r (roots (s (mutator m')))⦈, sys := s sys⦇heap := (sys_heap s)(r ↦ obj)⦈))
 = mut_m.tso_store_refs m s"
  "mut_m.tso_store_refs m (s(mutator m' := s (mutator m')⦇ghost_honorary_root := Option.set_option opt_r', ref := opt_r'⦈))
 = mut_m.tso_store_refs m s"
  "mut_m.tso_store_refs m (s(sys := s sys⦇heap := (sys_heap s)(r := map_option (λobj. obj⦇obj_fields := (obj_fields obj)(f := opt_r')⦈) (sys_heap s r)),
                                          mem_store_buffers := (mem_store_buffers (s sys))(p := ws)⦈))
 = (if p = mutator m then ⋃w ∈ set ws. store_refs w else mut_m.tso_store_refs m s)"
  "mut_m.tso_store_refs m (s(sys := s sys⦇heap := (sys_heap s)(r := map_option (λobj. obj⦇obj_payload := (obj_payload obj)(f := pl)⦈) (sys_heap s r)),
                                          mem_store_buffers := (mem_store_buffers (s sys))(p := ws)⦈))
 = (if p = mutator m then ⋃w ∈ set ws. store_refs w else mut_m.tso_store_refs m s)"
  "sys_mem_store_buffers p s = mw_Mark r fl # ws
⟹ mut_m.tso_store_refs m (s(sys := s sys⦇heap := (sys_heap s)(r := map_option (obj_mark_update (λ_. fl)) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)⦈))
 = mut_m.tso_store_refs m s"
unfolding mut_m.tso_store_refs_def by (auto simp: fun_upd_apply)

lemma fold_stores_points_to[rule_format, simplified conj_explode]:
  "heap (fold_stores ws (s sys)) r = Some obj ∧ obj_fields obj f = Some r'
     ⟶ (r points_to r') s ∨ (∃w ∈ set ws. r' ∈ store_refs w)" (is "?P (fold_stores ws) obj")
unfolding fold_stores_def
apply (rule spec[OF fold_invariant[where P="λfr. ∀obj. ?P fr obj" and Q="λw. w ∈ set ws"]])
  apply fastforce
 apply (fastforce simp: ran_def split: obj_at_splits)
apply clarsimp
apply (drule (1) bspec)
apply (clarsimp simp: fun_upd_apply split: mem_store_action.split_asm if_splits)
done

lemma points_to_Mutate:
  "(x points_to y)
         (s(sys := (s sys)⦇ heap := (sys_heap s)(r := map_option (λobj. obj⦇obj_fields := (obj_fields obj)(f := opt_r')⦈) (sys_heap s r)),
                            mem_store_buffers := (mem_store_buffers (s sys))(p := ws) ⦈))
  ⟷ (r ≠ x ∧ (x points_to y) s) ∨ (r = x ∧ valid_ref r s ∧ (opt_r' = Some y ∨ ( (x points_to y) s ∧ obj_at (λobj. ∃f'. obj_fields obj f' = Some y ∧ f ≠ f') r s)))"
unfolding ran_def by (auto simp: fun_upd_apply split: obj_at_splits)


subsection‹ FIXME mutator handshake facts ›

lemma ― ‹Sanity›
  "hp' = hs_step hp ⟹ ∃in' ht. (in', ht, hp', hp) ∈ hp_step_rel"
by (cases hp) (auto simp: hp_step_rel_def)

lemma ― ‹Sanity›
  "(False, ht, hp', hp) ∈ hp_step_rel ⟹ hp' = hp_step ht hp"
by (cases ht) (auto simp: hp_step_rel_def)

lemma (in mut_m) handshake_phase_invD:
  assumes "handshake_phase_inv s"
  shows "(sys_ghost_hs_in_sync m s, sys_hs_type s, sys_ghost_hs_phase s, mut_ghost_hs_phase s) ∈ hp_step_rel
       ∧ (sys_hs_pending m s ⟶ ¬sys_ghost_hs_in_sync m s)"
using assms unfolding handshake_phase_inv_def by simp

lemma handshake_in_syncD:
  "⟦ All (ghost_hs_in_sync (s sys)); handshake_phase_inv s ⟧
     ⟹ ∀m'. mut_m.mut_ghost_hs_phase m' s = sys_ghost_hs_phase s"
by clarsimp (auto simp: hp_step_rel_def dest!: mut_m.handshake_phase_invD)

lemmas fM_rel_invD = iffD1[OF fun_cong[OF fM_rel_inv_def[simplified atomize_eq]]]

text‹

Relate @{const "sys_ghost_hs_phase"}, @{const "gc_phase"},
@{const "sys_phase"} and writes to the phase in the GC's TSO buffer.

›

simps_of_case handshake_phase_rel_simps[simp]: handshake_phase_rel_def (splits: hs_phase.split)

lemma phase_rel_invD:
  assumes "phase_rel_inv s"
  shows "(∀m. sys_ghost_hs_in_sync m s, sys_ghost_hs_phase s, gc_phase s, sys_phase s, tso_pending_phase gc s) ∈ phase_rel"
using assms unfolding phase_rel_inv_def by simp

lemma mut_m_not_idle_no_fM_write:
  "⟦ ghost_hs_phase (s (mutator m)) ≠ hp_Idle; fM_rel_inv s; handshake_phase_inv s; tso_store_inv s; p ≠ sys ⟧
     ⟹ ¬sys_mem_store_buffers p s = mw_fM fl # ws"
apply (drule mut_m.handshake_phase_invD[where m=m])
apply (drule fM_rel_invD)
apply (clarsimp simp: hp_step_rel_def fM_rel_def filter_empty_conv p_not_sys)
apply (metis list.set_intros(1) tso_store_invD(4))
done

lemma (in mut_m) mut_ghost_handshake_phase_idle:
  "⟦ mut_ghost_hs_phase s = hp_Idle; handshake_phase_inv s; phase_rel_inv s ⟧
     ⟹ sys_phase s = ph_Idle"
apply (drule phase_rel_invD)
apply (drule handshake_phase_invD)
apply (auto simp: phase_rel_def hp_step_rel_def)
done

lemma mut_m_not_idle_no_fM_writeD:
  "⟦ sys_mem_store_buffers p s = mw_fM fl # ws; ghost_hs_phase (s (mutator m)) ≠ hp_Idle; fM_rel_inv s; handshake_phase_inv s; tso_store_inv s; p ≠ sys ⟧
     ⟹ False"
apply (drule mut_m.handshake_phase_invD[where m=m])
apply (drule fM_rel_invD)
apply (clarsimp simp: hp_step_rel_def fM_rel_def filter_empty_conv p_not_sys)
apply (metis list.set_intros(1) tso_store_invD(4))
done


subsection‹points to, reaches, reachable mut›

lemma (in mut_m) reachable_eq_imp:
  "eq_imp (λr'. mut_roots ❙⊗ mut_ghost_honorary_root ❙⊗ (λs. ⋃(ran ` obj_fields ` set_option (sys_heap s r')))
              ❙⊗ tso_pending_mutate (mutator m))
          (reachable r)"
unfolding eq_imp_def reachable_def tso_store_refs_def
apply clarsimp
apply (rename_tac s s')
apply (subgoal_tac "∀r'. (∃w∈set (sys_mem_store_buffers (mutator m) s). r' ∈ store_refs w) ⟷ (∃w∈set (sys_mem_store_buffers (mutator m) s'). r' ∈ store_refs w)")
 apply (subgoal_tac "∀x. (x reaches r) s ⟷ (x reaches r) s'")
  apply (clarsimp; fail)
 apply (auto simp: reaches_fields; fail)[1]
apply (drule arg_cong[where f=set])
apply (clarsimp simp: set_eq_iff)
apply (rule iffI)
 apply clarsimp
 apply (rename_tac s s' r' w)
 apply (drule_tac x=w in spec)
 apply (rule_tac x=w in bexI)
  apply (clarsimp; fail)
 apply (clarsimp split: mem_store_action.splits; fail)
apply clarsimp
apply (rename_tac s s' r' w)
apply (drule_tac x=w in spec)
apply (rule_tac x=w in bexI)
 apply (clarsimp; fail)
apply (clarsimp split: mem_store_action.splits; fail)
done

lemmas reachable_fun_upd[simp] = eq_imp_fun_upd[OF mut_m.reachable_eq_imp, simplified eq_imp_simps, rule_format]

lemma reachableI[intro]:
  "x ∈ mut_m.mut_roots m s ⟹ mut_m.reachable m x s"
  "x ∈ mut_m.tso_store_refs m s ⟹ mut_m.reachable m x s"
by (auto simp: mut_m.reachable_def reaches_def)

lemma reachable_points_to[elim]:
  "⟦ (x points_to y) s; mut_m.reachable m x s ⟧ ⟹ mut_m.reachable m y s"
by (auto simp: mut_m.reachable_def reaches_def elim: rtranclp.intros(2))

lemma (in mut_m) mut_reachableE[consumes 1, case_names mut_root tso_store_refs]:
  "⟦ reachable y s;
     ⋀x. ⟦ (x reaches y) s; x ∈ mut_roots s ⟧ ⟹ Q;
     ⋀x. ⟦ (x reaches y) s; x ∈ mut_ghost_honorary_root s ⟧ ⟹ Q;
     ⋀x. ⟦ (x reaches y) s; x ∈ tso_store_refs s ⟧ ⟹ Q ⟧ ⟹ Q"
by (auto simp: reachable_def)

lemma reachable_induct[consumes 1, case_names root ghost_honorary_root tso_root reaches]:
  assumes r: "mut_m.reachable m y s"
  assumes root: "⋀x. ⟦ x ∈ mut_m.mut_roots m s ⟧ ⟹ P x"
  assumes ghost_honorary_root: "⋀x. ⟦ x ∈ mut_m.mut_ghost_honorary_root m s ⟧ ⟹ P x"
  assumes tso_root: "⋀x. x ∈ mut_m.tso_store_refs m s ⟹ P x"
  assumes reaches: "⋀x y. ⟦ mut_m.reachable m x s; (x points_to y) s; P x ⟧ ⟹ P y"
  shows "P y"
using r unfolding mut_m.reachable_def
proof(clarify)
  fix x
  assume "(x reaches y) s" and "x ∈ mut_m.mut_roots m s ∪ mut_m.mut_ghost_honorary_root m s ∪ mut_m.tso_store_refs m s"
  then show "P y"
  unfolding reaches_def proof induct
    case base with root ghost_honorary_root tso_root show ?case by blast
  next
    case (step y z) with reaches show ?case
      unfolding mut_m.reachable_def reaches_def by meson
  qed
qed

lemma mutator_reachable_tso:
  "sys_mem_store_buffers (mutator m) s = mw_Mutate r f opt_r' # ws
    ⟹ mut_m.reachable m r s ∧ (∀r'. opt_r' = Some r' ⟶ mut_m.reachable m r' s)"
  "sys_mem_store_buffers (mutator m) s = mw_Mutate_Payload r f pl # ws
    ⟹ mut_m.reachable m r s"
by (auto simp: mut_m.tso_store_refs_def)


subsection‹ Colours ›

lemma greyI[intro]:
  "r ∈ ghost_honorary_grey (s p) ⟹ grey r s"
  "r ∈ W (s p) ⟹ grey r s"
  "r ∈ WL p s ⟹ grey r s"
unfolding grey_def WL_def by (case_tac [!] p) auto

lemma blackD[dest]:
  "black r s ⟹ marked r s"
  "black r s ⟹ r ∉ WL p s"
unfolding black_def grey_def by simp_all

lemma whiteI[intro]: (* FIXME simp normal form of def *)
  "obj_at (λobj. obj_mark obj = (¬ sys_fM s)) r s ⟹ white r s"
unfolding white_def by simp

lemma marked_not_white[dest]:
  "white r s ⟹ ¬marked r s"
unfolding white_def by (simp_all split: obj_at_splits)

lemma white_valid_ref[elim!]:
  "white r s ⟹ valid_ref r s"
unfolding white_def by (simp_all split: obj_at_splits)

lemma not_white_marked[elim!]:
  "⟦¬ white r s; valid_ref r s⟧ ⟹ marked r s"
unfolding white_def by (simp split: obj_at_splits)

lemma black_eq_imp:
  "eq_imp (λ_::unit. (λs. r ∈ (⋃p. WL p s)) ❙⊗ sys_fM ❙⊗ (λs. map_option obj_mark (sys_heap s r)))
          (black r)"
unfolding eq_imp_def black_def grey_def by (auto split: obj_at_splits)

lemma grey_eq_imp:
  "eq_imp (λ_::unit. (λs. r ∈ (⋃p. WL p s)))
          (grey r)"
unfolding eq_imp_def grey_def by auto

lemma white_eq_imp:
  "eq_imp (λ_::unit. sys_fM ❙⊗ (λs. map_option obj_mark (sys_heap s r)))
          (white r)"
unfolding eq_imp_def white_def by (auto split: obj_at_splits)

lemmas black_fun_upd[simp] = eq_imp_fun_upd[OF black_eq_imp, simplified eq_imp_simps, rule_format]
lemmas grey_fun_upd[simp] = eq_imp_fun_upd[OF grey_eq_imp, simplified eq_imp_simps, rule_format]
lemmas white_fun_upd[simp] = eq_imp_fun_upd[OF white_eq_imp, simplified eq_imp_simps, rule_format]


text‹coloured heaps›

lemma black_heap_eq_imp:
  "eq_imp (λr'. (λs. ⋃p. WL p s) ❙⊗ sys_fM ❙⊗ (λs. map_option obj_mark (sys_heap s r')))
          black_heap"
apply (clarsimp simp: eq_imp_def black_heap_def black_def grey_def all_conj_distrib fun_eq_iff split: option.splits)
apply (rename_tac s s')
apply (subgoal_tac "∀x. marked x s ⟷ marked x s'")
 apply (subgoal_tac "∀x. valid_ref x s ⟷ valid_ref x s'")
  apply (subgoal_tac "∀x. (∀p. x ∉ WL p s) ⟷ (∀p. x ∉ WL p s')")
   apply clarsimp
  apply (auto simp: set_eq_iff)[1]
 apply clarsimp
 apply (rename_tac x)
 apply (rule eq_impD[OF obj_at_eq_imp])
 apply (drule_tac x=x in spec)
 apply (drule_tac f="map_option ⟨True⟩" in arg_cong)
 apply fastforce
apply clarsimp
apply (rule eq_impD[OF obj_at_eq_imp])
apply clarsimp
apply (rename_tac x)
apply (drule_tac x=x in spec)
apply (drule_tac f="map_option (λfl. fl = sys_fM s)" in arg_cong)
apply simp
done

lemma white_heap_eq_imp:
  "eq_imp (λr'. sys_fM ❙⊗ (λs. map_option obj_mark (sys_heap s r')))
          white_heap"
apply (clarsimp simp: all_conj_distrib eq_imp_def white_def white_heap_def obj_at_def fun_eq_iff
               split: option.splits)
apply (rule iffI)
apply (metis (opaque_lifting, no_types) map_option_eq_Some)+
done

lemma no_black_refs_eq_imp:
  "eq_imp (λr'. (λs. (⋃p. WL p s)) ❙⊗ sys_fM ❙⊗ (λs. map_option obj_mark (sys_heap s r')))
          no_black_refs"
apply (clarsimp simp add: eq_imp_def no_black_refs_def black_def grey_def all_conj_distrib fun_eq_iff set_eq_iff split: option.splits)
apply (rename_tac s s')
apply (subgoal_tac "∀x. marked x s ⟷ marked x s'")
 apply clarsimp
apply (clarsimp split: obj_at_splits)
apply (rename_tac x)
apply (drule_tac x=x in spec)+
apply (auto split: obj_at_splits)
done

lemmas black_heap_fun_upd[simp] = eq_imp_fun_upd[OF black_heap_eq_imp, simplified eq_imp_simps, rule_format]
lemmas white_heap_fun_upd[simp] = eq_imp_fun_upd[OF white_heap_eq_imp, simplified eq_imp_simps, rule_format]
lemmas no_black_refs_fun_upd[simp] = eq_imp_fun_upd[OF no_black_refs_eq_imp, simplified eq_imp_simps, rule_format]

lemma white_heap_imp_no_black_refs[elim!]:
  "white_heap s ⟹ no_black_refs s"
apply (clarsimp simp: white_def white_heap_def no_black_refs_def black_def)
apply (rename_tac x)
apply (drule_tac x=x in spec)
apply (clarsimp split: obj_at_splits)
done

lemma black_heap_no_greys[elim]:
  "⟦ no_grey_refs s; ∀r. marked r s ∨ ¬valid_ref r s ⟧ ⟹ black_heap s"
unfolding black_def black_heap_def no_grey_refs_def by fastforce

lemma heap_colours_colours:
  "black_heap s ⟹ ¬white r s"
  "white_heap s ⟹ ¬black r s"
by (auto simp: black_heap_def white_def white_heap_def
        dest!: spec[where x=r]
        split: obj_at_splits)


text‹The strong-tricolour invariant ›

lemma strong_tricolour_invD:
  "⟦ black x s; (x points_to y) s; valid_ref y s; strong_tricolour_inv s ⟧
     ⟹ marked y s"
unfolding strong_tricolour_inv_def by fastforce

lemma no_black_refsD:
  "no_black_refs s ⟹ ¬black r s"
unfolding no_black_refs_def by simp

lemma has_white_path_to_induct[consumes 1, case_names refl step, induct set: has_white_path_to]:
  assumes "(x has_white_path_to y) s"
  assumes "⋀x. P x x"
  assumes "⋀x y z. ⟦(x has_white_path_to y) s; P x y; (y points_to z) s; white z s⟧ ⟹ P x z"
  shows "P x y"
using assms unfolding has_white_path_to_def by (rule rtranclp.induct; blast)

lemma has_white_path_toD[dest]:
  "(x has_white_path_to y) s ⟹ white y s ∨ x = y"
unfolding has_white_path_to_def by (fastforce elim: rtranclp.cases)

lemma has_white_path_to_refl[iff]:
  "(x has_white_path_to x) s"
unfolding has_white_path_to_def by simp

lemma has_white_path_to_step[intro]:
  "⟦(x has_white_path_to y) s; (y points_to z) s; white z s⟧ ⟹ (x has_white_path_to z) s"
  "⟦(y has_white_path_to z) s; (x points_to y) s; white y s⟧ ⟹ (x has_white_path_to z) s"
unfolding has_white_path_to_def
 apply (simp add: rtranclp.rtrancl_into_rtrancl)
apply (simp add: converse_rtranclp_into_rtranclp)
done

lemma has_white_path_toE[elim!]:
  "⟦ (x points_to y) s; white y s ⟧ ⟹ (x has_white_path_to y) s"
unfolding has_white_path_to_def by (auto elim: rtranclp.intros(2))

lemma has_white_path_to_reaches[elim]:
  "(x has_white_path_to y) s ⟹ (x reaches y) s"
unfolding has_white_path_to_def reaches_def
by (induct rule: rtranclp.induct) (auto intro: rtranclp.intros(2))

lemma has_white_path_to_blacken[simp]:
  "(x has_white_path_to w) (s(gc := s gc⦇ W := gc_W s - rs ⦈)) ⟷ (x has_white_path_to w) s"
unfolding has_white_path_to_def by (simp add: fun_upd_apply)

lemma has_white_path_to_eq_imp': ― ‹Complicated condition takes care of ‹alloc›: collapses no object and object with no fields›
  assumes "(x has_white_path_to y) s'"
  assumes "∀r'. ⋃(ran ` obj_fields ` set_option (sys_heap s' r')) = ⋃(ran ` obj_fields ` set_option (sys_heap s r'))"
  assumes "∀r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r')"
  assumes "sys_fM s' = sys_fM s"
  shows "(x has_white_path_to y) s"
using assms
proof induct
  case (step x y z)
  then have "(y points_to z) s"
    by (cases "sys_heap s y")
       (auto 10 10 simp: ran_def obj_at_def split: option.splits dest!: spec[where x=y])
  with step show ?case
apply -
apply (rule has_white_path_to_step, assumption, assumption)
apply (clarsimp simp: white_def split: obj_at_splits)
apply (metis map_option_eq_Some option.sel)
done
qed simp

lemma has_white_path_to_eq_imp:
  "eq_imp (λr'. sys_fM ❙⊗ (λs. ⋃(ran ` obj_fields ` set_option (sys_heap s r'))) ❙⊗ (λs. map_option obj_mark (sys_heap s r')))
          (x has_white_path_to y)"
unfolding eq_imp_def
apply (clarsimp simp: all_conj_distrib)
apply (rule iffI)
 apply (erule has_white_path_to_eq_imp'; auto)
apply (erule has_white_path_to_eq_imp'; auto)
done

lemmas has_white_path_to_fun_upd[simp] = eq_imp_fun_upd[OF has_white_path_to_eq_imp, simplified eq_imp_simps, rule_format]


text‹grey protects white›

lemma grey_protects_whiteD[dest]:
  "(g grey_protects_white w) s ⟹ grey g s ∧ (g = w ∨ white w s)"
by (auto simp: grey_protects_white_def)

lemma grey_protects_whiteI[iff]:
  "grey g s ⟹ (g grey_protects_white g) s"
by (simp add: grey_protects_white_def)

lemma grey_protects_whiteE[elim!]:
  "⟦ (g points_to w) s; grey g s; white w s ⟧ ⟹ (g grey_protects_white w) s"
  "⟦ (g grey_protects_white y) s; (y points_to w) s; white w s ⟧ ⟹ (g grey_protects_white w) s"
by (auto simp: grey_protects_white_def)

lemma grey_protects_white_reaches[elim]:
  "(g grey_protects_white w) s ⟹ (g reaches w) s"
by (auto simp: grey_protects_white_def)

lemma grey_protects_white_induct[consumes 1, case_names refl step, induct set: grey_protects_white]:
  assumes "(g grey_protects_white w) s"
  assumes "⋀x. grey x s ⟹ P x x"
  assumes "⋀x y z. ⟦(x has_white_path_to y) s; P x y; (y points_to z) s; white z s⟧ ⟹ P x z"
  shows "P g w"
using assms unfolding grey_protects_white_def
apply -
apply (elim conjE)
apply (rotate_tac -1)
apply (induct rule: has_white_path_to_induct)
apply blast+
done


subsection‹ @{term "valid_W_inv"} ›

lemma valid_W_inv_sys_ghg_empty_iff[elim!]:
  "valid_W_inv s ⟹ sys_ghost_honorary_grey s = {}"
unfolding valid_W_inv_def by simp

lemma WLI[intro]:
  "r ∈ W (s p) ⟹ r ∈ WL p s"
  "r ∈ ghost_honorary_grey (s p) ⟹ r ∈ WL p s"
unfolding WL_def by simp_all

lemma WL_eq_imp:
  "eq_imp (λ(_::unit) s. (ghost_honorary_grey (s p), W (s p)))
          (WL p)"
unfolding eq_imp_def WL_def by simp

lemmas WL_fun_upd[simp] = eq_imp_fun_upd[OF WL_eq_imp, simplified eq_imp_simps, rule_format]

lemma valid_W_inv_eq_imp:
  "eq_imp (λ(p, r). (λs. W (s p)) ❙⊗ (λs. ghost_honorary_grey (s p)) ❙⊗ sys_fM ❙⊗ (λs. map_option obj_mark (sys_heap s r)) ❙⊗ sys_mem_lock ❙⊗ tso_pending_mark p)
          valid_W_inv"
apply (clarsimp simp: eq_imp_def valid_W_inv_def fun_eq_iff all_conj_distrib white_def)
apply (rename_tac s s')
apply (subgoal_tac "∀p. WL p s = WL p s'")
 apply (subgoal_tac "∀x. marked x s ⟷ marked x s'")
  apply (subgoal_tac "∀x. obj_at (λobj. obj_mark obj = (¬sys_fM s')) x s ⟷ obj_at (λobj. obj_mark obj = (¬sys_fM s')) x s'")
   apply (subgoal_tac "∀x xa xb. mw_Mark xa xb ∈ set (sys_mem_store_buffers x s) ⟷ mw_Mark xa xb ∈ set (sys_mem_store_buffers x s')")
    apply (simp; fail)
   apply clarsimp
   apply (rename_tac x xa xb)
   apply (drule_tac x=x in spec, drule arg_cong[where f=set], fastforce)
  apply (clarsimp split: obj_at_splits)
  apply (rename_tac x)
  apply ( (drule_tac x=x in spec)+ )[1]
  apply (case_tac "sys_heap s x", simp_all)
   apply (case_tac "sys_heap s' x", auto)[1]
 apply (clarsimp split: obj_at_splits)
 apply (rename_tac x)
 apply (drule_tac x=x in spec)
 apply (case_tac "sys_heap s x", simp_all)
 apply (case_tac "sys_heap s' x", simp_all)
apply (simp add: WL_def)
done

lemmas valid_W_inv_fun_upd[simp] = eq_imp_fun_upd[OF valid_W_inv_eq_imp, simplified eq_imp_simps, rule_format]

lemma valid_W_invE[elim!]:
  "⟦ r ∈ W (s p); valid_W_inv s ⟧ ⟹ marked r s"
  "⟦ r ∈ ghost_honorary_grey (s p); sys_mem_lock s ≠ Some p; valid_W_inv s ⟧ ⟹ marked r s"
  "⟦ r ∈ W (s p); valid_W_inv s ⟧ ⟹ valid_ref r s"
  "⟦ r ∈ ghost_honorary_grey (s p); sys_mem_lock s ≠ Some p; valid_W_inv s ⟧ ⟹ valid_ref r s"
  "⟦ mw_Mark r fl ∈ set (sys_mem_store_buffers p s); valid_W_inv s ⟧ ⟹ r ∈ ghost_honorary_grey (s p)"
unfolding valid_W_inv_def
apply (simp_all add:  split: obj_at_splits)
apply blast+
done

lemma valid_W_invD:
  "⟦ sys_mem_store_buffers p s = mw_Mark r fl # ws; valid_W_inv s ⟧
     ⟹ fl = sys_fM s ∧ r ∈ ghost_honorary_grey (s p) ∧ tso_locked_by p s ∧ white r s ∧ filter is_mw_Mark ws = []"
  "⟦ mw_Mark r fl ∈ set (sys_mem_store_buffers p s); valid_W_inv s ⟧
     ⟹ fl = sys_fM s ∧ r ∈ ghost_honorary_grey (s p) ∧ tso_locked_by p s ∧ white r s ∧ filter is_mw_Mark (sys_mem_store_buffers p s) = [mw_Mark r fl]"
unfolding valid_W_inv_def white_def by (clarsimp dest!: spec[where x=p], blast)+

lemma valid_W_inv_colours:
  "⟦white x s; valid_W_inv s⟧ ⟹ x ∉ W (s p)"
using marked_not_white valid_W_invE(1) by force

lemma valid_W_inv_no_mark_stores_invD:
  "⟦ sys_mem_lock s ≠ Some p; valid_W_inv s ⟧
     ⟹ tso_pending p is_mw_Mark s = []"
by (auto dest: valid_W_invD(2) intro!: filter_False)

lemma valid_W_inv_sys_load[simp]:
  "⟦ sys_mem_lock s ≠ Some p; valid_W_inv s ⟧
     ⟹ sys_load p (mr_Mark r) (s sys) = mv_Mark (map_option obj_mark (sys_heap s r))"
unfolding sys_load_def fold_stores_def
apply clarsimp
apply (rule fold_invariant[where P="λfr. map_option obj_mark (heap (fr (s sys)) r) = map_option obj_mark (sys_heap s r)"
                             and Q="λw. ∀r fl. w ≠ mw_Mark r fl"])
  apply (auto simp: map_option_case do_store_action_def filter_empty_conv fun_upd_apply
              dest: valid_W_invD(2)
             split: mem_store_action.splits option.splits)
done


subsection‹ ‹grey_reachable› ›

lemma grey_reachable_eq_imp:
  "eq_imp (λr'. (λs. ⋃p. WL p s) ❙⊗ (λs. Set.bind (Option.set_option (sys_heap s r')) (ran ∘ obj_fields)))
          (grey_reachable r)"
by (auto simp: eq_imp_def grey_reachable_def grey_def set_eq_iff reaches_fields)

lemmas grey_reachable_fun_upd[simp] = eq_imp_fun_upd[OF grey_reachable_eq_imp, simplified eq_imp_simps, rule_format]

lemma grey_reachableI[intro]:
  "grey g s ⟹ grey_reachable g s"
unfolding grey_reachable_def reaches_def by blast

lemma grey_reachableE:
  "⟦ (g points_to y) s; grey_reachable g s ⟧ ⟹ grey_reachable y s"
unfolding grey_reachable_def reaches_def by (auto elim: rtranclp.intros(2))


subsection‹valid refs inv›

lemma valid_refs_invI:
  "⟦ ⋀m x y. ⟦ (x reaches y) s; mut_m.root m x s ∨ grey x s ⟧ ⟹ valid_ref y s
   ⟧ ⟹ valid_refs_inv s"
by (auto simp: valid_refs_inv_def mut_m.reachable_def grey_reachable_def)

lemma valid_refs_inv_eq_imp:
  "eq_imp (λ(m', r'). (λs. roots (s (mutator m'))) ❙⊗ (λs. ghost_honorary_root (s (mutator m'))) ❙⊗ (λs. map_option obj_fields (sys_heap s r')) ❙⊗ tso_pending_mutate (mutator m') ❙⊗ (λs. ⋃p. WL p s))
          valid_refs_inv"
apply (clarsimp simp: eq_imp_def valid_refs_inv_def grey_reachable_def all_conj_distrib)
apply (rename_tac s s')
apply (subgoal_tac "∀r'. valid_ref r' s ⟷ valid_ref r' s'")
 apply (subgoal_tac "∀r'. ⋃(ran ` obj_fields ` set_option (sys_heap s r')) = ⋃(ran ` obj_fields ` set_option (sys_heap s' r'))")
  apply (subst eq_impD[OF mut_m.reachable_eq_imp])
   defer
   apply (subst eq_impD[OF grey_eq_imp])
    defer
    apply (subst eq_impD[OF reaches_eq_imp])
     defer
     apply force
    apply (metis option.set_map)
   apply (clarsimp split: obj_at_splits)
   apply (metis (no_types, opaque_lifting) None_eq_map_option_iff option.exhaust)
  apply clarsimp
 apply clarsimp
apply clarsimp
done

lemmas valid_refs_inv_fun_upd[simp] = eq_imp_fun_upd[OF valid_refs_inv_eq_imp, simplified eq_imp_simps, rule_format]

lemma valid_refs_invD[elim]:
  "⟦ x ∈ mut_m.mut_roots m s; (x reaches y) s; valid_refs_inv s ⟧ ⟹ valid_ref y s"
  "⟦ x ∈ mut_m.mut_roots m s; (x reaches y) s; valid_refs_inv s ⟧ ⟹ ∃obj. sys_heap s y = Some obj"
  "⟦ x ∈ mut_m.tso_store_refs m s; (x reaches y) s; valid_refs_inv s ⟧ ⟹ valid_ref y s"
  "⟦ x ∈ mut_m.tso_store_refs m s; (x reaches y) s; valid_refs_inv s ⟧ ⟹ ∃obj. sys_heap s y = Some obj"
  "⟦ w ∈ set (sys_mem_store_buffers (mutator m) s); x ∈ store_refs w; (x reaches y) s; valid_refs_inv s ⟧ ⟹ valid_ref y s"
  "⟦ w ∈ set (sys_mem_store_buffers (mutator m) s); x ∈ store_refs w; (x reaches y) s; valid_refs_inv s ⟧ ⟹ ∃obj. sys_heap s y = Some obj"
  "⟦ grey x s; (x reaches y) s; valid_refs_inv s ⟧ ⟹ valid_ref y s"
  "⟦ mut_m.reachable m x s; valid_refs_inv s ⟧ ⟹ valid_ref x s"
  "⟦ mut_m.reachable m x s; valid_refs_inv s ⟧ ⟹ ∃obj. sys_heap s x = Some obj"
  "⟦ x ∈ mut_m.mut_ghost_honorary_root m s; (x reaches y) s; valid_refs_inv s ⟧ ⟹ valid_ref y s"
  "⟦ x ∈ mut_m.mut_ghost_honorary_root m s; (x reaches y) s; valid_refs_inv s ⟧ ⟹ ∃obj. sys_heap s y = Some obj"
apply (simp_all add: valid_refs_inv_def grey_reachable_def mut_m.reachable_def mut_m.tso_store_refs_def
              split: obj_at_splits)
apply blast+
done


text‹reachable snapshot inv›

context mut_m
begin

lemma reachable_snapshot_invI[intro]:
  "(⋀y. reachable y s ⟹ in_snapshot y s) ⟹ reachable_snapshot_inv s"
by (simp add: reachable_snapshot_inv_def)

lemma reachable_snapshot_inv_eq_imp:
  "eq_imp (λr'. mut_roots ❙⊗ mut_ghost_honorary_root ❙⊗ (λs. r' ∈ (⋃p. WL p s)) ❙⊗ sys_fM
            ❙⊗ (λs. ⋃(ran ` obj_fields ` set_option (sys_heap s r'))) ❙⊗ (λs. map_option obj_mark (sys_heap s r'))
            ❙⊗ tso_pending_mutate (mutator m))
          reachable_snapshot_inv"
unfolding eq_imp_def mut_m.reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def black_def grey_def
apply (clarsimp simp: all_conj_distrib)
apply (rename_tac s s')
apply (subst (1) eq_impD[OF has_white_path_to_eq_imp])
 apply force
apply (subst eq_impD[OF reachable_eq_imp])
 apply force
apply (subgoal_tac "∀x. obj_at (λobj. obj_mark obj = sys_fM s') x s ⟷ obj_at (λobj. obj_mark obj = sys_fM s') x s'")
 apply force
apply (clarsimp split: obj_at_splits)
apply (rename_tac x)
apply (drule_tac x=x in spec)+
apply (case_tac "sys_heap s x", simp_all)
apply (case_tac "sys_heap s' x", simp_all)
done

end

lemmas reachable_snapshot_fun_upd[simp] = eq_imp_fun_upd[OF mut_m.reachable_snapshot_inv_eq_imp, simplified eq_imp_simps, rule_format]

lemma in_snapshotI[intro]:
  "black r s ⟹ in_snapshot r s"
  "grey r s ⟹ in_snapshot r s"
  "⟦ white w s; (g grey_protects_white w) s ⟧ ⟹ in_snapshot w s"
by (auto simp: in_snapshot_def)

lemma ― ‹Sanity›
  "in_snapshot r s ⟹ black r s ∨ grey r s ∨ white r s"
by (auto simp: in_snapshot_def)

lemma in_snapshot_valid_ref:
  "⟦ in_snapshot r s; valid_refs_inv s ⟧ ⟹ valid_ref r s"
by (metis blackD(1) grey_protects_whiteD grey_protects_white_reaches in_snapshot_def obj_at_cong obj_at_def option.case(2) valid_refs_invD(7))

lemma reachableI2[intro]:
  "x ∈ mut_m.mut_ghost_honorary_root m s ⟹ mut_m.reachable m x s"
unfolding mut_m.reachable_def reaches_def by blast

lemma tso_pending_mw_mutate_cong:
  "⟦ filter is_mw_Mutate (sys_mem_store_buffers p s) = filter is_mw_Mutate (sys_mem_store_buffers p s');
     ⋀r f r'. P r f r' ⟷ Q r f r' ⟧
     ⟹ (∀r f r'. mw_Mutate r f r' ∈ set (sys_mem_store_buffers p s)  ⟶ P r f r')
     ⟷ (∀r f r'. mw_Mutate r f r' ∈ set (sys_mem_store_buffers p s') ⟶ Q r f r')"
by (intro iff_allI) (auto dest!: arg_cong[where f=set])

lemma (in mut_m) marked_insertions_eq_imp:
  "eq_imp (λr'. sys_fM ❙⊗ (λs. map_option obj_mark (sys_heap s r')) ❙⊗ tso_pending_mw_mutate (mutator m))
          marked_insertions"
unfolding eq_imp_def marked_insertions_def obj_at_def
apply (clarsimp split: mem_store_action.splits)
apply (erule tso_pending_mw_mutate_cong)
apply (clarsimp split: option.splits obj_at_splits)
apply (rename_tac s s' opt x)
apply (drule_tac x=x in spec)
apply auto
done

lemmas marked_insertions_fun_upd[simp] = eq_imp_fun_upd[OF mut_m.marked_insertions_eq_imp, simplified eq_imp_simps, rule_format]

lemma marked_insertionD[elim!]:
  "⟦ sys_mem_store_buffers (mutator m) s = mw_Mutate r f (Some r') # ws; mut_m.marked_insertions m s ⟧
     ⟹ marked r' s"
by (auto simp: mut_m.marked_insertions_def)

lemma marked_insertions_store_buffer_empty[intro]:
  "tso_pending_mutate (mutator m) s = [] ⟹ mut_m.marked_insertions m s"
unfolding mut_m.marked_insertions_def by (auto simp: filter_empty_conv split: mem_store_action.splits)

(* marked_deletions *)

lemma (in mut_m) marked_deletions_eq_imp:
  "eq_imp (λr'. sys_fM ❙⊗ (λs. map_option obj_fields (sys_heap s r')) ❙⊗ (λs. map_option obj_mark (sys_heap s r')) ❙⊗ tso_pending_mw_mutate (mutator m))
          marked_deletions"
unfolding eq_imp_def marked_deletions_def obj_at_field_on_heap_def ran_def
apply (clarsimp simp: all_conj_distrib)
apply (drule arg_cong[where f=set])
apply (subgoal_tac "∀x. marked x s ⟷ marked x s'")
 apply (clarsimp cong: option.case_cong)
 apply (rule iffI; clarsimp simp: set_eq_iff split: option.splits mem_store_action.splits; blast)
apply clarsimp
apply (rename_tac s s' x)
apply (drule_tac x=x in spec)+
apply (force split: obj_at_splits)
done

lemmas marked_deletions_fun_upd[simp] = eq_imp_fun_upd[OF mut_m.marked_deletions_eq_imp, simplified eq_imp_simps, rule_format]

lemma marked_deletions_store_buffer_empty[intro]:
  "tso_pending_mutate (mutator m) s = [] ⟹ mut_m.marked_deletions m s"
unfolding mut_m.marked_deletions_def by (auto simp: filter_empty_conv split: mem_store_action.splits)


subsection‹Location-specific simplification rules›

lemma obj_at_ref_sweep_loop_free[simp]:
  "obj_at P r (s(sys := (s sys)⦇heap := (sys_heap s)(r' := None)⦈)) ⟷ obj_at P r s ∧ r ≠ r'"
by (clarsimp simp: fun_upd_apply split: obj_at_splits)

lemma obj_at_alloc[simp]:
  "sys_heap s r' = None
  ⟹ obj_at P r (s(m := mut_m_s', sys := (s sys)⦇ heap := (sys_heap s)(r' ↦ obj) ⦈))
  ⟷ (obj_at P r s ∨ (r = r' ∧ P obj))"
unfolding ran_def by (simp add: fun_upd_apply split: obj_at_splits)

lemma valid_ref_valid_null_ref_simps[simp]:
  "valid_ref r (s(sys := do_store_action w (s sys)⦇mem_store_buffers := (mem_store_buffers (s sys))(p := ws)⦈)) ⟷ valid_ref r s"
  "valid_null_ref r' (s(sys := do_store_action w (s sys)⦇mem_store_buffers := (mem_store_buffers (s sys))(p := ws)⦈)) ⟷ valid_null_ref r' s"
  "valid_null_ref r' (s(mutator m := mut_s', sys := (s sys)⦇ heap := (heap (s sys))(r'' ↦ obj) ⦈)) ⟷ valid_null_ref r' s ∨ r' = Some r''"
unfolding do_store_action_def valid_null_ref_def
by (auto simp: fun_upd_apply
        split: mem_store_action.splits obj_at_splits option.splits)

context mut_m
begin

lemma reachable_load[simp]:
  assumes "sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref r'"
  assumes "r ∈ mut_roots s"
  shows "mut_m.reachable m' y (s(mutator m := s (mutator m)⦇ roots := mut_roots s ∪ Option.set_option r' ⦈)) ⟷ mut_m.reachable m' y s" (is "?lhs = ?rhs")
proof(cases "m' = m")
  case True show ?thesis
  proof(rule iffI)
    assume ?lhs with assms True show ?rhs
unfolding sys_load_def
apply clarsimp
apply (clarsimp simp: reachable_def reaches_def tso_store_refs_def sys_load_def fold_stores_def fun_upd_apply)
apply (elim disjE)
   apply blast
  defer
 apply blast
apply blast

apply (fold fold_stores_def)
apply clarsimp
apply (drule (1) fold_stores_points_to)
apply (erule disjE)
 apply (fastforce elim!: converse_rtranclp_into_rtranclp[rotated] split: obj_at_splits intro!: ranI)
apply (clarsimp split: mem_store_action.splits)
apply meson
done
  next
    assume ?rhs with True show ?lhs unfolding mut_m.reachable_def by (fastforce simp: fun_upd_apply)
  qed
qed (simp add: fun_upd_apply)

end

text‹WL›

lemma WL_blacken[simp]:
  "gc_ghost_honorary_grey s = {}
    ⟹ WL p (s(gc := s gc⦇ W := gc_W s - rs ⦈)) = WL p s - { r |r. p = gc ∧ r ∈ rs }"
unfolding WL_def by (auto simp: fun_upd_apply)

lemma WL_hs_done[simp]:
  "ghost_honorary_grey (s (mutator m)) = {}
     ⟹ WL p (s(mutator m := s (mutator m)⦇ W := {}, ghost_hs_phase := hp' ⦈,
                 sys   := s sys⦇ hs_pending := hsp', W := sys_W s ∪ W (s (mutator m)),
                                 ghost_hs_in_sync := in' ⦈))
      = (case p of gc ⇒ WL gc s | mutator m' ⇒ (if m' = m then {} else WL (mutator m') s) | sys ⇒ WL sys s ∪ WL (mutator m) s)"
  "ghost_honorary_grey (s (mutator m)) = {}
     ⟹ WL p (s(mutator m := s (mutator m)⦇ W := {} ⦈,
                 sys   := s sys⦇ hs_pending := hsp', W := sys_W s ∪ W (s (mutator m)),
                                 ghost_hs_in_sync := in' ⦈))
      = (case p of gc ⇒ WL gc s | mutator m' ⇒ (if m' = m then {} else WL (mutator m') s) | sys ⇒ WL sys s ∪ WL (mutator m) s)"
unfolding WL_def by (auto simp: fun_upd_apply split: process_name.splits)

lemma colours_load_W[iff]:
  "gc_W s = {} ⟹ black r (s(gc := (s gc)⦇W := W (s sys)⦈, sys := (s sys)⦇W := {}⦈)) ⟷ black r s"
  "gc_W s = {} ⟹ grey r (s(gc := (s gc)⦇W := W (s sys)⦈, sys := (s sys)⦇W := {}⦈)) ⟷ grey r s"
unfolding black_def grey_def WL_def
apply (simp_all add: fun_upd_apply)
apply safe
apply (case_tac [!] x)
apply blast+
done

lemma WL_load_W[simp]:
  "gc_W s = {}
    ⟹ (WL p (s(gc := (s gc)⦇W := sys_W s⦈, sys := (s sys)⦇W := {}⦈)))
     = (case p of gc ⇒ WL gc s ∪ sys_W s | mutator m ⇒ WL (mutator m) s | sys ⇒ sys_ghost_honorary_grey s)"
unfolding WL_def by (auto simp: fun_upd_apply split: process_name.splits)

text‹no grey refs›

lemma no_grey_refs_eq_imp:
  "eq_imp (λ(_::unit). (λs. ⋃p. WL p s))
          no_grey_refs"
by (auto simp add: eq_imp_def grey_def no_grey_refs_def set_eq_iff)

lemmas no_grey_refs_fun_upd[simp] = eq_imp_fun_upd[OF no_grey_refs_eq_imp, simplified eq_imp_simps, rule_format]

lemma no_grey_refs_no_pending_marks:
  "⟦ no_grey_refs s; valid_W_inv s ⟧ ⟹ tso_no_pending_marks s"
unfolding no_grey_refs_def by (auto intro!: filter_False dest: valid_W_invD(2))

lemma no_grey_refs_not_grey_reachableD:
  "no_grey_refs s ⟹ ¬grey_reachable x s"
by (clarsimp simp: no_grey_refs_def grey_reachable_def)

lemma no_grey_refsD:
  "no_grey_refs s ⟹ r ∉ W (s p)"
  "no_grey_refs s ⟹ r ∉ WL p s"
  "no_grey_refs s ⟹ r ∉ ghost_honorary_grey (s p)"
by (auto simp: no_grey_refs_def)

lemma no_grey_refs_marked[dest]:
  "⟦ marked r s; no_grey_refs s ⟧ ⟹ black r s"
by (auto simp: no_grey_refs_def black_def)

lemma no_grey_refs_bwD[dest]:
  "⟦ heap (s sys) r = Some obj; no_grey_refs s ⟧ ⟹ black r s ∨ white r s"
by (clarsimp simp: black_def grey_def no_grey_refs_def white_def split: obj_at_splits)

context mut_m
begin

lemma reachable_blackD:
  "⟦ no_grey_refs s; reachable_snapshot_inv s; reachable r s ⟧ ⟹ black r s"
by (simp add: no_grey_refs_def reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def)

lemma no_grey_refs_not_reachable:
  "⟦ no_grey_refs s; reachable_snapshot_inv s; white r s ⟧ ⟹ ¬reachable r s"
by (fastforce simp: no_grey_refs_def reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def
             split: obj_at_splits)

lemma no_grey_refs_not_rootD:
  "⟦ no_grey_refs s; reachable_snapshot_inv s; white r s ⟧
     ⟹ r ∉ mut_roots s ∧ r ∉ mut_ghost_honorary_root s ∧ r ∉ tso_store_refs s"
apply (drule (2) no_grey_refs_not_reachable)
apply (force simp: reachable_def reaches_def)
done

lemma reachable_snapshot_inv_white_root:
  "⟦ white w s; w ∈ mut_roots s ∨ w ∈ mut_ghost_honorary_root s; reachable_snapshot_inv s ⟧ ⟹ ∃g. (g grey_protects_white w) s"
unfolding reachable_snapshot_inv_def in_snapshot_def reachable_def grey_protects_white_def reaches_def by auto

end

(* colours *)

lemma black_dequeue_Mark[simp]:
  "black b (s(sys := (s sys)⦇ heap := (sys_heap s)(r := map_option (obj_mark_update (λ_. fl)) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws) ⦈))
⟷ (black b s ∧ b ≠ r) ∨ (b = r ∧ fl = sys_fM s ∧ valid_ref r s ∧ ¬grey r s)"
unfolding black_def by (auto simp: fun_upd_apply split: obj_at_splits)

lemma colours_sweep_loop_free[iff]:
  "black r (s(sys := s sys⦇heap := (heap (s sys))(r' := None)⦈)) ⟷ (black r s ∧ r ≠ r')"
  "grey r (s(sys := s sys⦇heap := (heap (s sys))(r' := None)⦈)) ⟷ (grey r s)"
  "white r (s(sys := s sys⦇heap := (heap (s sys))(r' := None)⦈)) ⟷ (white r s ∧ r ≠ r')"
unfolding black_def grey_def white_def by (auto simp: fun_upd_apply split: obj_at_splits)

lemma colours_get_work_done[simp]:
  "black r (s(mutator m := (s (mutator m))⦇W := {}⦈,
              sys := (s sys)⦇ hs_pending := hp', W := W (s sys) ∪ W (s (mutator m)),
                              ghost_hs_in_sync := his' ⦈)) ⟷ black r s"
  "grey r (s(mutator m := (s (mutator m))⦇W := {}⦈,
              sys := (s sys)⦇ hs_pending := hp', W := W (s sys) ∪ W (s (mutator m)),
                              ghost_hs_in_sync := his' ⦈)) ⟷ grey r s"
  "white r (s(mutator m := (s (mutator m))⦇W := {}⦈,
              sys := (s sys)⦇ hs_pending := hp', W := W (s sys) ∪ W (s (mutator m)),
                              ghost_hs_in_sync := his' ⦈)) ⟷ white r s"
unfolding black_def grey_def WL_def
apply (simp_all add: fun_upd_apply split: obj_at_splits)
 apply blast
apply (metis process_name.distinct(3))
done

lemma colours_get_roots_done[simp]:
  "black r (s(mutator m := (s (mutator m))⦇ W := {}, ghost_hs_phase := hs' ⦈,
              sys := (s sys)⦇ hs_pending := hp', W := W (s sys) ∪ W (s (mutator m)),
                              ghost_hs_in_sync := his' ⦈)) ⟷ black r s"
  "grey r (s(mutator m := (s (mutator m))⦇ W := {}, ghost_hs_phase := hs' ⦈,
              sys := (s sys)⦇ hs_pending := hp', W := W (s sys) ∪ W (s (mutator m)),
                              ghost_hs_in_sync := his' ⦈)) ⟷ grey r s"
  "white r (s(mutator m := (s (mutator m))⦇ W := {}, ghost_hs_phase := hs' ⦈,
              sys := (s sys)⦇ hs_pending := hp', W := W (s sys) ∪ W (s (mutator m)),
                              ghost_hs_in_sync := his' ⦈)) ⟷ white r s"
unfolding black_def grey_def WL_def
apply (simp_all add: fun_upd_apply split: obj_at_splits)
 apply blast
apply (metis process_name.distinct(3))
done

lemma colours_flip_fM[simp]:
  "fl ≠ sys_fM s ⟹ black b (s(sys := (s sys)⦇fM := fl, mem_store_buffers := (mem_store_buffers (s sys))(p := ws)⦈)) ⟷ white b s ∧ ¬grey b s"
unfolding black_def white_def by (simp add: fun_upd_apply)

lemma colours_alloc[simp]:
  "heap (s sys) r' = None
     ⟹ black r (s(mutator m := (s (mutator m))⦇ roots := roots' ⦈, sys := (s sys)⦇heap := (heap (s sys))(r' ↦ ⦇obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty⦈)⦈))
     ⟷ black r s ∨ (r' = r ∧ fl = sys_fM s ∧ ¬grey r' s)"
  "grey r (s(mutator m := (s (mutator m))⦇ roots := roots' ⦈, sys := (s sys)⦇heap := (heap (s sys))(r' ↦ ⦇obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty⦈)⦈))
     ⟷ grey r s"
  "heap (s sys) r' = None
     ⟹ white r (s(mutator m := (s (mutator m))⦇ roots := roots' ⦈, sys := (s sys)⦇heap := (heap (s sys))(r' ↦ ⦇obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty⦈)⦈))
     ⟷ white r s ∨ (r' = r ∧ fl ≠ sys_fM s)"
unfolding black_def white_def by (auto simp: fun_upd_apply split: obj_at_splits)

lemma heap_colours_alloc[simp]:
  "⟦ heap (s sys) r' = None; valid_refs_inv s ⟧
  ⟹ black_heap (s(mutator m := s (mutator m)⦇roots := roots'⦈, sys := s sys⦇heap := (sys_heap s)(r' ↦ ⦇obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty⦈)⦈))
  ⟷ black_heap s ∧ fl = sys_fM s"
  "heap (s sys) r' = None
  ⟹ white_heap (s(mutator m := s (mutator m)⦇roots := roots'⦈, sys := s sys⦇heap := (sys_heap s)(r' ↦ ⦇obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty⦈)⦈))
  ⟷ white_heap s ∧ fl ≠ sys_fM s"
unfolding black_heap_def white_def white_heap_def
apply (simp_all add: fun_upd_apply split: obj_at_splits)
 apply (rule iffI)
  apply (intro allI conjI impI)
   apply (rename_tac x)
   apply (drule_tac x=x in spec)
   apply clarsimp
  apply (drule spec[where x=r'], auto simp: reaches_def dest!: valid_refs_invD split: obj_at_splits)[2]
apply (rule iffI)
 apply (intro allI conjI impI)
  apply (rename_tac x obj)
  apply (drule_tac x=x in spec)
  apply clarsimp
 apply (drule spec[where x=r'], auto dest!: valid_refs_invD split: obj_at_splits)[2]
done

lemma grey_protects_white_hs_done[simp]:
  "(g grey_protects_white w) (s(mutator m := s (mutator m)⦇ W := {}, ghost_hs_phase := hs' ⦈,
                              sys := s sys⦇ hs_pending := hp', W := sys_W s ∪ W (s (mutator m)),
                                            ghost_hs_in_sync := his' ⦈))
  ⟷ (g grey_protects_white w) s"
unfolding grey_protects_white_def by (simp add: fun_upd_apply)

lemma grey_protects_white_alloc[simp]:
  "⟦ fl = sys_fM s; sys_heap s r = None ⟧
     ⟹ (g grey_protects_white w) (s(mutator m := s (mutator m)⦇roots := roots'⦈, sys := s sys⦇heap := (sys_heap s)(r ↦ ⦇obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty⦈)⦈))
     ⟷ (g grey_protects_white w) s"
unfolding grey_protects_white_def has_white_path_to_def by simp

lemma (in mut_m) reachable_snapshot_inv_sweep_loop_free:
  fixes s :: "('field, 'mut, 'payload, 'ref) lsts"
  assumes nmr: "white r s"
  assumes ngs: "no_grey_refs s"
  assumes rsi: "reachable_snapshot_inv s"
  shows "reachable_snapshot_inv (s(sys := (s sys)⦇heap := (heap (s sys))(r := None)⦈))" (is "reachable_snapshot_inv ?s'")
proof
  fix y :: "'ref"
  assume rx: "reachable y ?s'"
  then have "black y s ∧ y ≠ r"
  proof(induct rule: reachable_induct)
    case (root x) with ngs nmr rsi show ?case
      by (auto simp: fun_upd_apply dest: reachable_blackD)
  next
    case (ghost_honorary_root x) with ngs nmr rsi show ?case
      unfolding reachable_def reaches_def by (auto simp: fun_upd_apply dest: reachable_blackD)
  next
    case (tso_root x) with ngs nmr rsi show ?case
      unfolding reachable_def reaches_def by (auto simp: fun_upd_apply dest: reachable_blackD)
  next
    case (reaches x y) with ngs nmr rsi show ?case
      unfolding reachable_def reaches_def
      apply (clarsimp simp: fun_upd_apply)
      apply (drule predicate2D[OF rtranclp_mono[where s="λx y. (x points_to y) s", OF predicate2I], rotated])
       apply (clarsimp split: obj_at_splits if_splits)
      apply (rule conjI)
       apply (rule reachable_blackD, assumption, assumption)
       apply (simp add: reachable_def reaches_def)
       apply (blast intro: rtranclp.intros(2))
      apply clarsimp
      apply (frule (1) reachable_blackD[where r=r])
       apply (simp add: reachable_def reaches_def)
       apply (blast intro: rtranclp.intros(2))
      apply auto
      done
  qed
  then show "in_snapshot y ?s'"
    unfolding in_snapshot_def by simp
qed

lemma reachable_alloc[simp]:
  assumes rn: "sys_heap s r = None"
  shows "mut_m.reachable m r' (s(mutator m' := (s (mutator m'))⦇roots := insert r (roots (s (mutator m')))⦈, sys := (s sys)⦇heap := (sys_heap s)(r ↦ ⦇obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty⦈)⦈))
     ⟷ mut_m.reachable m r' s ∨ (m' = m ∧ r' = r)" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  assume ?lhs from this assms show ?rhs
  proof(induct rule: reachable_induct)
    case (reaches x y) then show ?case by clarsimp (fastforce simp: mut_m.reachable_def reaches_def elim: rtranclp.intros(2) split: obj_at_splits)
  qed (auto simp: fun_upd_apply split: if_splits)
next
  assume ?rhs then show ?lhs
  proof(rule disjE)
    assume "mut_m.reachable m r' s" then show ?thesis
    proof(induct rule: reachable_induct)
      case (tso_root x) then show ?case
        unfolding mut_m.reachable_def by fastforce
    next
      case (reaches x y) with rn show ?case
        unfolding mut_m.reachable_def by fastforce
    qed (auto simp: fun_upd_apply)
  next
    assume "m' = m ∧ r' = r" with rn show ?thesis
      unfolding mut_m.reachable_def by (fastforce simp: fun_upd_apply)
  qed
qed

context mut_m
begin

lemma reachable_snapshot_inv_alloc[simp, elim!]:
  fixes s :: "('field, 'mut, 'payload, 'ref) lsts"
  assumes rsi: "reachable_snapshot_inv s"
  assumes rn: "sys_heap s r = None"
  assumes fl: "fl = sys_fM s"
  assumes vri: "valid_refs_inv s"
  shows "reachable_snapshot_inv (s(mutator m' := (s (mutator m'))⦇roots := insert r (roots (s (mutator m')))⦈, sys := (s sys)⦇heap := (sys_heap s)(r ↦ ⦇obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty⦈)⦈))"
(is "reachable_snapshot_inv ?s'")
using assms unfolding reachable_snapshot_inv_def in_snapshot_def
by (auto simp del: reachable_fun_upd)

lemma reachable_snapshot_inv_discard_roots[simp]:
  "⟦ reachable_snapshot_inv s; roots' ⊆ roots (s (mutator m)) ⟧
     ⟹ reachable_snapshot_inv (s(mutator m := (s (mutator m))⦇roots := roots'⦈))"
unfolding reachable_snapshot_inv_def reachable_def in_snapshot_def grey_protects_white_def by (auto simp: fun_upd_apply)

lemma reachable_snapshot_inv_load[simp]:
  "⟦ reachable_snapshot_inv s; sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref r'; r ∈ mut_roots s ⟧
     ⟹ reachable_snapshot_inv (s(mutator m := s (mutator m)⦇ roots := mut_roots s ∪ Option.set_option r' ⦈))"
unfolding reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def by (simp add: fun_upd_apply)

lemma reachable_snapshot_inv_store_ins[simp]:
  "⟦ reachable_snapshot_inv s; r ∈ mut_roots s; (∃r'. opt_r' = Some r') ⟶ the opt_r' ∈ mut_roots s ⟧
     ⟹ reachable_snapshot_inv (s(mutator m := s (mutator m)⦇ghost_honorary_root := {}⦈,
                                  sys := s sys⦇  mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r']) ⦈))"
unfolding reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def reachable_def
apply clarsimp
apply (drule_tac x=x in spec)
apply (auto simp: fun_upd_apply)
(* FIXME what's gone wrong here? *)
apply (subst (asm) tso_store_refs_simps; force)+
done

end

lemma WL_mo_co_mark[simp]:
  "ghost_honorary_grey (s p) = {}
     ⟹ WL p' (s(p := s p⦇ ghost_honorary_grey := rs ⦈)) = WL p' s ∪ { r |r. p' = p ∧ r ∈ rs}"
unfolding WL_def by (simp add: fun_upd_apply)

lemma ghost_honorary_grey_mo_co_mark[simp]:
  "⟦ ghost_honorary_grey (s p) = {} ⟧ ⟹ black b (s(p := s p⦇ghost_honorary_grey := {r}⦈)) ⟷ black b s ∧ b ≠ r"
  "⟦ ghost_honorary_grey (s p) = {} ⟧ ⟹ grey g (s(p := (s p)⦇ghost_honorary_grey := {r}⦈)) ⟷ grey g s ∨ g = r"
  "⟦ ghost_honorary_grey (s p) = {} ⟧ ⟹ white w (s(p := s p⦇ghost_honorary_grey := {r}⦈))  ⟷ white w s"
unfolding black_def grey_def by (auto simp: fun_upd_apply)

lemma ghost_honorary_grey_mo_co_W[simp]:
  "ghost_honorary_grey (s p') = {r}
     ⟹ (WL p (s(p' := (s p')⦇W := insert r (W (s p')), ghost_honorary_grey := {}⦈))) = (WL p s)"
  "ghost_honorary_grey (s p') = {r}
     ⟹ grey g (s(p' := (s p')⦇W := insert r (W (s p')), ghost_honorary_grey := {}⦈)) ⟷ grey g s"
unfolding grey_def WL_def by (auto simp: fun_upd_apply split: process_name.splits if_splits)

lemma reachable_sweep_loop_free:
  "mut_m.reachable m r (s(sys := s sys⦇heap := (sys_heap s)(r' := None)⦈))
   ⟹ mut_m.reachable m r s"
unfolding mut_m.reachable_def reaches_def by (clarsimp simp: fun_upd_apply) (metis (no_types, lifting) mono_rtranclp)

lemma reachable_deref_del[simp]:
  "⟦ sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref opt_r'; r ∈ mut_m.mut_roots m s; mut_m.mut_ghost_honorary_root m s = {} ⟧
   ⟹ mut_m.reachable m' y (s(mutator m := s (mutator m)⦇ ghost_honorary_root := Option.set_option opt_r', ref := opt_r' ⦈))
   ⟷ mut_m.reachable m' y s"
unfolding mut_m.reachable_def reaches_def sys_load_def
apply (clarsimp simp: fun_upd_apply)
apply (rule iffI)
 apply clarsimp
 apply (elim disjE)
   apply metis
  apply (erule option_bind_invE; auto dest!: fold_stores_points_to)
 apply (auto elim!: converse_rtranclp_into_rtranclp[rotated]
              simp: mut_m.tso_store_refs_def)
done

lemma no_black_refs_dequeue[simp]:
  "⟦ sys_mem_store_buffers p s = mw_Mark r fl # ws; no_black_refs s; valid_W_inv s ⟧
   ⟹ no_black_refs (s(sys := s sys⦇heap := (sys_heap s)(r := map_option (obj_mark_update (λ_. fl)) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)⦈))"
  "⟦ sys_mem_store_buffers p s = mw_Mutate r f r' # ws; no_black_refs s ⟧
     ⟹ no_black_refs (s(sys := s sys⦇heap := (sys_heap s)(r := map_option (λobj. obj⦇obj_fields := (obj_fields obj)(f := r')⦈) (sys_heap s r)),
                                      mem_store_buffers := (mem_store_buffers (s sys))(p := ws)⦈))"
unfolding no_black_refs_def by (auto simp: fun_upd_apply dest: valid_W_invD)

lemma colours_blacken[simp]:
  "valid_W_inv s ⟹ black b (s(gc := s gc⦇W := gc_W s - {r}⦈)) ⟷ black b s ∨ (r ∈ gc_W s ∧ b = r)"
  "⟦ r ∈ gc_W s; valid_W_inv s ⟧ ⟹ grey g (s(gc := s gc⦇W := gc_W s - {r}⦈)) ⟷ (grey g s ∧ g ≠ r)"
  (*  "white w (s(gc := s gc⦇W := gc_W s - {r}⦈)) ⟷ white w s" is redundant *)
unfolding black_def grey_def valid_W_inv_def
apply (simp_all add: all_conj_distrib split: obj_at_splits if_splits)
apply safe
apply (simp_all add: WL_def fun_upd_apply split: if_splits)
  apply (metis option.distinct(1))
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply metis
done
(* FIXME
apply (auto simp: black_def grey_def WL_def split: obj_at_splits)
apply metis+
done
*)

lemma no_black_refs_alloc[simp]:
  "⟦ heap (s sys) r' = None; no_black_refs s ⟧
     ⟹ no_black_refs (s(mutator m' := s (mutator m')⦇roots := roots'⦈, sys := s sys⦇heap := (sys_heap s)(r' ↦ ⦇obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty⦈)⦈))
     ⟷ fl ≠ sys_fM s ∨ grey r' s"
unfolding no_black_refs_def by simp

lemma no_black_refs_mo_co_mark[simp]:
  "⟦ ghost_honorary_grey (s p) = {}; white r s ⟧
     ⟹ no_black_refs (s(p := s p⦇ghost_honorary_grey := {r}⦈)) ⟷ no_black_refs s"
unfolding no_black_refs_def by auto

lemma grey_protects_white_mark[simp]:
  assumes ghg: "ghost_honorary_grey (s p) = {}"
  shows "(∃g. (g grey_protects_white w) (s(p := s p⦇ ghost_honorary_grey := {r} ⦈)))
      ⟷ (∃g'. (g' grey_protects_white w) s) ∨ (r has_white_path_to w) s" (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  then obtain g where "(g grey_protects_white w) (s(p := s p⦇ghost_honorary_grey := {r}⦈))" by blast
  from this ghg show ?rhs by induct (auto simp: fun_upd_apply)
next
  assume ?rhs then show ?lhs
  proof(safe)
    fix g assume "(g grey_protects_white w) s"
    from this ghg show ?thesis
apply induct
 apply force
unfolding grey_protects_white_def
apply (auto simp: fun_upd_apply)
done
  next
    assume "(r has_white_path_to w) s" with ghg show ?thesis
      unfolding grey_protects_white_def has_white_path_to_def by (auto simp: fun_upd_apply)
  qed
qed

lemma valid_refs_inv_dequeue_Mutate:
  fixes s :: "('field, 'mut, 'payload, 'ref) lsts"
  assumes vri: "valid_refs_inv s"
  assumes sb: "sys_mem_store_buffers (mutator m') s = mw_Mutate r f opt_r' # ws"
  shows "valid_refs_inv (s(sys := s sys⦇heap := (sys_heap s)(r := map_option (λobj. obj⦇obj_fields := (obj_fields obj)(f := opt_r')⦈) (sys_heap s r)),
                                        mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)⦈))" (is "valid_refs_inv ?s'")
proof(rule valid_refs_invI)
  fix m
  let ?root = "λm x. mut_m.root m x ❙∨ grey x"
  fix x y assume xy: "(x reaches y) ?s'" and x: "?root m x ?s'"
  from xy have "(∃m x. ?root m x s ∧ (x reaches y) s) ∧ valid_ref y ?s'"
  unfolding reaches_def proof induct
    case base with x sb vri show ?case
      apply -
      apply (subst obj_at_fun_upd)
       apply (auto simp: mut_m.tso_store_refs_def reaches_def fun_upd_apply split: if_splits intro: valid_refs_invD(5)[where m=m])
      apply (metis list.set_intros(2) rtranclp.rtrancl_refl)
      done (* FIXME rules *)
  next
    case (step y z)
    with sb vri show ?case
      apply -
      apply (subst obj_at_fun_upd, clarsimp simp: fun_upd_apply)
      apply (subst (asm) obj_at_fun_upd, fastforce simp: fun_upd_apply)
      apply (clarsimp simp: points_to_Mutate fun_upd_apply)
      apply (fastforce elim: rtranclp.intros(2) simp: mut_m.tso_store_refs_def reaches_def fun_upd_apply intro: exI[where x=m'] valid_refs_invD(5)[where m=m'])
      done
   qed
  then show "valid_ref y ?s'" by blast
qed

lemma valid_refs_inv_dequeue_Mutate_Payload:
  notes if_split_asm[split del]
  fixes s :: "('field, 'mut, 'payload, 'ref) lsts"
  assumes vri: "valid_refs_inv s"
  assumes sb: "sys_mem_store_buffers (mutator m') s = mw_Mutate_Payload r f pl # ws"
  shows "valid_refs_inv (s(sys := s sys⦇heap := (sys_heap s)(r := map_option (λobj. obj⦇obj_payload := (obj_payload obj)(f := pl)⦈) (sys_heap s r)),
                                        mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)⦈))" (is "valid_refs_inv ?s'")
apply (rule valid_refs_invI)
using assms
apply (clarsimp simp: valid_refs_invD fun_upd_apply split: obj_at_splits mem_store_action.splits)
apply auto
 apply (metis (mono_tags, lifting) UN_insert Un_iff list.simps(15) mut_m.tso_store_refs_def valid_refs_invD(4))
apply (metis case_optionE obj_at_def valid_refs_invD(7))
done

(*<*)

end
(*>*)