Theory Proofs_Basis

(*<*)
(*
 * 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 Proofs_Basis
imports
  Model
  "HOL-Library.Simps_Case_Conv"
begin

(* From 40e16c534243 by Makarius. Doesn't seem to have a huge impact on run time now (2021-01-07) *)
declare subst_all [simp del] [[simproc del: defined_all]]

(*>*)
section‹ Proofs Basis \label{sec:proofs-basis}›

text‹

Extra HOL.

›

lemma Set_bind_insert[simp]:
  "Set.bind (insert a A) B = B a ∪ (Set.bind A B)"
by (auto simp: Set.bind_def)

lemma option_bind_invE[elim]:
  "⟦ Option.bind f g = None; ⋀a. ⟦ f = Some a; g a = None ⟧ ⟹ Q; f = None ⟹ Q ⟧ ⟹ Q"
  "⟦ Option.bind f g = Some x; ⋀a. ⟦ f = Some a; g a = Some x ⟧ ⟹ Q ⟧ ⟹ Q"
by (case_tac [!] f) simp_all

lemmas conj_explode = conj_imp_eq_imp_imp

text‹

Tweak the default simpset:
▪ "not in dom" as a premise negates the goal
▪ we always want to execute suffix
▪ we try to make simplification rules about @{const ‹fun_upd›} more stable

›

declare dom_def[simp]
declare suffix_to_prefix[simp]
declare map_option.compositionality[simp]
declare o_def[simp]
declare Option.Option.option.set_map[simp]
declare bind_image[simp]

declare fun_upd_apply[simp del]
declare fun_upd_same[simp]
declare fun_upd_other[simp]

declare gc_phase.case_cong[cong]
declare mem_store_action.case_cong[cong]
declare process_name.case_cong[cong]
declare hs_phase.case_cong[cong]
declare hs_type.case_cong[cong]

declare if_split_asm[split]

text‹

Collect the component definitions. Inline everything. This is what the proofs work on.
Observe we lean heavily on locales.

›

context gc
begin

lemmas all_com_defs =
  (* gc.com_def *) handshake_done_def handshake_init_def handshake_noop_def handshake_get_roots_def handshake_get_work_def
  mark_object_fn_def

lemmas com_def2 = com_def[simplified all_com_defs append.simps if_True if_False]

intern_com com_def2

end

context mut_m
begin

lemmas all_com_defs =
  (* mut.com_def *) mut_m.handshake_def mut_m.store_def
  mark_object_fn_def

lemmas com_def2 = mut_m.com_def[simplified all_com_defs append.simps if_True if_False]

intern_com com_def2

end

context sys
begin

lemmas all_com_defs =
  (* sys.com_def *) sys.alloc_def sys.free_def sys.mem_TSO_def sys.handshake_def

lemmas com_def2 = com_def[simplified all_com_defs append.simps if_True if_False]

intern_com com_def2

end

lemmas all_com_interned_defs = gc.com_interned mut_m.com_interned sys.com_interned

named_theorems inv "Location-sensitive invariant definitions"
named_theorems nie "Non-interference elimination rules"


subsection‹ Model-specific functions and predicates ›

text‹

We define a pile of predicates and accessor functions for the
process's local states. One might hope that a more sophisticated
approach would automate all of this (cf \<^citet>‹"DBLP:journals/entcs/SchirmerW09"›).

›

abbreviation prefixed :: "location ⇒ location set" where
  "prefixed p ≡ { l . prefix p l }"

abbreviation suffixed :: "location ⇒ location set" where
  "suffixed p ≡ { l . suffix p l }"

abbreviation "is_mw_Mark w ≡ ∃r fl. w = mw_Mark r fl"
abbreviation "is_mw_Mutate w ≡ ∃r f r'. w = mw_Mutate r f r'"
abbreviation "is_mw_Mutate_Payload w ≡ ∃r f pl. w = mw_Mutate_Payload r f pl"
abbreviation "is_mw_fA w ≡ ∃fl. w = mw_fA fl"
abbreviation "is_mw_fM w ≡ ∃fl. w = mw_fM fl"
abbreviation "is_mw_Phase w ≡ ∃ph. w = mw_Phase ph"

abbreviation (input) pred_in_W :: "'ref ⇒ 'mut process_name ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" (infix ‹in'_W› 50) where
  "r in_W p ≡ λs. r ∈ W (s p)"

abbreviation (input) pred_in_ghost_honorary_grey :: "'ref ⇒ 'mut process_name ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" (infix ‹in'_ghost'_honorary'_grey› 50) where
  "r in_ghost_honorary_grey p ≡ λs. r ∈ ghost_honorary_grey (s p)"

abbreviation "gc_cas_mark s ≡ cas_mark (s gc)"
abbreviation "gc_fM s ≡ fM (s gc)"
abbreviation "gc_field s ≡ field (s gc)"
abbreviation "gc_field_set s ≡ field_set (s gc)"
abbreviation "gc_mark s ≡ mark (s gc)"
abbreviation "gc_mut s ≡ mut (s gc)"
abbreviation "gc_muts s ≡ muts (s gc)"
abbreviation "gc_phase s ≡ phase (s gc)"
abbreviation "gc_tmp_ref s ≡ tmp_ref (s gc)"
abbreviation "gc_ghost_honorary_grey s ≡ ghost_honorary_grey (s gc)"
abbreviation "gc_ref s ≡ ref (s gc)"
abbreviation "gc_refs s ≡ refs (s gc)"
abbreviation "gc_the_ref ≡ the ∘ gc_ref"
abbreviation "gc_W s ≡ W (s gc)"

abbreviation at_gc :: "location ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred ⇒ ('field, 'mut, 'payload, 'ref) gc_pred" where
  "at_gc l P ≡ at gc l ❙⟶ LSTP P"

abbreviation atS_gc :: "location set ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred ⇒ ('field, 'mut, 'payload, 'ref) gc_pred" where
  "atS_gc ls P ≡ atS gc ls ❙⟶ LSTP P"

context mut_m
begin

abbreviation at_mut :: "location ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred ⇒ ('field, 'mut, 'payload, 'ref) gc_pred" where
  "at_mut l P ≡ at (mutator m) l ❙⟶ LSTP P"

abbreviation atS_mut :: "location set ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred ⇒ ('field, 'mut, 'payload, 'ref) gc_pred" where
  "atS_mut ls P ≡ atS (mutator m) ls ❙⟶ LSTP P"

abbreviation "mut_cas_mark s ≡ cas_mark (s (mutator m))"
abbreviation "mut_field s ≡ field (s (mutator m))"
abbreviation "mut_fM s ≡ fM (s (mutator m))"
abbreviation "mut_ghost_honorary_grey s ≡ ghost_honorary_grey (s (mutator m))"
abbreviation "mut_ghost_hs_phase s ≡ ghost_hs_phase (s (mutator m))"
abbreviation "mut_ghost_honorary_root s ≡ ghost_honorary_root (s (mutator m))"
abbreviation "mut_hs_pending s ≡ mutator_hs_pending (s (mutator m))"
abbreviation "mut_hs_type s ≡ hs_type (s (mutator m))"
abbreviation "mut_mark s ≡ mark (s (mutator m))"
abbreviation "mut_new_ref s ≡ new_ref (s (mutator m))"
abbreviation "mut_phase s ≡ phase (s (mutator m))"
abbreviation "mut_ref s ≡ ref (s (mutator m))"
abbreviation "mut_tmp_ref s ≡ tmp_ref (s (mutator m))"
abbreviation "mut_the_new_ref ≡ the ∘ mut_new_ref"
abbreviation "mut_the_ref ≡ the ∘ mut_ref"
abbreviation "mut_refs s ≡ refs (s (mutator m))"
abbreviation "mut_roots s ≡ roots (s (mutator m))"
abbreviation "mut_W s ≡ W (s (mutator m))"

end

abbreviation sys_heap :: "('field, 'mut, 'payload, 'ref) lsts ⇒ 'ref ⇒ ('field, 'payload, 'ref) object option" where "sys_heap s ≡ heap (s sys)"

abbreviation "sys_fA s ≡ fA (s sys)"
abbreviation "sys_fM s ≡ fM (s sys)"
abbreviation "sys_ghost_honorary_grey s ≡ ghost_honorary_grey (s sys)"
abbreviation "sys_ghost_hs_in_sync m s ≡ ghost_hs_in_sync (s sys) m"
abbreviation "sys_ghost_hs_phase s ≡ ghost_hs_phase (s sys)"
abbreviation "sys_hs_pending m s ≡ hs_pending (s sys) m"
abbreviation "sys_hs_type s ≡ hs_type (s sys)"
abbreviation "sys_mem_store_buffers p s ≡ mem_store_buffers (s sys) p"
abbreviation "sys_mem_lock s ≡ mem_lock (s sys)"
abbreviation "sys_phase s ≡ phase (s sys)"
abbreviation "sys_W s ≡ W (s sys)"

abbreviation atS_sys :: "location set ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred ⇒ ('field, 'mut, 'payload, 'ref) gc_pred" where
  "atS_sys ls P ≡ atS sys ls ❙⟶ LSTP P"

text‹Projections on TSO buffers.›

abbreviation (input) "tso_unlocked s ≡ mem_lock (s sys) = None"
abbreviation (input) "tso_locked_by p s ≡ mem_lock (s sys) = Some p"

abbreviation (input) "tso_pending p P s ≡ filter P (mem_store_buffers (s sys) p)"
abbreviation (input) "tso_pending_store p w s ≡ w ∈ set (mem_store_buffers (s sys) p)"

abbreviation (input) "tso_pending_fA p ≡ tso_pending p is_mw_fA"
abbreviation (input) "tso_pending_fM p ≡ tso_pending p is_mw_fM"
abbreviation (input) "tso_pending_mark p ≡ tso_pending p is_mw_Mark"
abbreviation (input) "tso_pending_mw_mutate p ≡ tso_pending p is_mw_Mutate"
abbreviation (input) "tso_pending_mutate p ≡ tso_pending p (is_mw_Mutate ❙∨ is_mw_Mutate_Payload)" ―‹ TSO makes it (mostly) not worth distinguishing these. ›
abbreviation (input) "tso_pending_phase p ≡ tso_pending p is_mw_Phase"

abbreviation (input) "tso_no_pending_marks ≡ ❙∀p. LIST_NULL (tso_pending_mark p)"

text‹

A somewhat-useful abstraction of the heap, following l4.verified,
which asserts that there is an object at the given reference with the
given property. In some sense this encodes a three-valued logic.

›

definition obj_at :: "(('field, 'payload, 'ref) object ⇒ bool) ⇒ 'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
  "obj_at P r ≡ λs. case sys_heap s r of None ⇒ False | Some obj ⇒ P obj"

abbreviation (input) valid_ref :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
  "valid_ref r ≡ obj_at ⟨True⟩ r"

definition valid_null_ref :: "'ref option ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
  "valid_null_ref r ≡ case r of None ⇒ ⟨True⟩ | Some r' ⇒ valid_ref r'"

abbreviation pred_points_to :: "'ref ⇒ 'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" (infix ‹points'_to› 51) where
  "x points_to y ≡ λs. obj_at (λobj. y ∈ ran (obj_fields obj)) x s"

text‹

We use Isabelle's standard transitive-reflexive closure to define
reachability through the heap.

›

definition reaches :: "'ref ⇒ 'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" (infix ‹reaches› 51) where
  "x reaches y = (λs. (λx y. (x points_to y) s)⇧*⇧* x y)"

text‹

The predicate ‹obj_at_field_on_heap› asserts that @{term ‹valid_ref r›}
and if ‹f› is a field of the object referred to by ‹r› then it it satisfies ‹P›.

›

definition obj_at_field_on_heap :: "('ref ⇒ bool) ⇒ 'ref ⇒ 'field ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
  "obj_at_field_on_heap P r f ≡ λs.
     case map_option obj_fields (sys_heap s r) of
         None ⇒ False
       | Some fs ⇒ (case fs f of None ⇒ True
                               | Some r' ⇒ P r')"


subsection‹Object colours›

text‹

We adopt the classical tricolour scheme for object colours due to
\<^citet>‹"DBLP:journals/cacm/DijkstraLMSS78"›, but
tweak it somewhat in the presence of worklists and TSO. Intuitively:
\begin{description}
\item[White] potential garbage, not yet reached
\item[Grey] reached, presumed live, a source of possible new references (work)
\item[Black] reached, presumed live, not a source of new references
\end{description}

In this particular setting we use the following interpretation:
\begin{description}
\item[White:] not marked
\item[Grey:] on a worklist or @{const ‹ghost_honorary_grey›}
\item[Black:] marked and not on a worklist
\end{description}

Note that this allows the colours to overlap: an object being marked
may be white (on the heap) and in @{const "ghost_honorary_grey"} for
some process, i.e. grey.

›

abbreviation marked :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
  "marked r s ≡ obj_at (λobj. obj_mark obj = sys_fM s) r s"

definition white :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
  "white r s ≡ obj_at (λobj. obj_mark obj ≠ sys_fM s) r s"

definition WL :: "'mut process_name ⇒ ('field, 'mut, 'payload, 'ref) lsts ⇒ 'ref set" where
  "WL p = (λs. W (s p) ∪ ghost_honorary_grey (s p))"

definition grey :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
  "grey r = (❙∃p. ⟨r⟩ ❙∈ WL p)"

definition black :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
  "black r ≡ marked r ❙∧ ❙¬grey r"

text‹ These demonstrate the overlap in colours. ›

lemma colours_distinct[dest]:
  "black r s ⟹ ¬grey r s"
  "black r s ⟹ ¬white r s"
  "grey r s  ⟹ ¬black r s"
  "white r s ⟹ ¬black r s"
by (auto simp: black_def white_def obj_at_def split: option.splits) (* FIXME invisible *)

lemma marked_imp_black_or_grey:
  "marked r s ⟹ black r s ∨ grey r s"
  "¬ white r s ⟹ ¬ valid_ref r s ∨ black r s ∨ grey r s"
by (auto simp: black_def grey_def white_def obj_at_def split: option.splits)  (* FIXME invisible *)

text‹

In some phases the heap is monochrome.

›

definition black_heap :: "('field, 'mut, 'payload, 'ref) lsts_pred" where
  "black_heap = (❙∀r. valid_ref r ❙⟶ black r)"

definition white_heap :: "('field, 'mut, 'payload, 'ref) lsts_pred" where
  "white_heap = (❙∀r. valid_ref r ❙⟶ white r)"

definition no_black_refs :: "('field, 'mut, 'payload, 'ref) lsts_pred" where
  "no_black_refs = (❙∀r. ❙¬black r)"

definition no_grey_refs :: "('field, 'mut, 'payload, 'ref) lsts_pred" where
  "no_grey_refs = (❙∀r. ❙¬grey r)"


subsection‹Reachability›

text‹

We treat pending TSO heap mutations as extra mutator roots.

›

abbreviation store_refs :: "('field, 'payload, 'ref) mem_store_action ⇒ 'ref set" where
  "store_refs w ≡ case w of mw_Mutate r f r' ⇒ {r} ∪ Option.set_option r' | mw_Mutate_Payload r f pl ⇒ {r} | _ ⇒ {}"

definition (in mut_m) tso_store_refs :: "('field, 'mut, 'payload, 'ref) lsts ⇒ 'ref set" where
  "tso_store_refs = (λs. ⋃w ∈ set (sys_mem_store_buffers (mutator m) s). store_refs w)"

abbreviation (in mut_m) root :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
  "root x ≡ ⟨x⟩ ❙∈ mut_roots ❙∪ mut_ghost_honorary_root ❙∪ tso_store_refs"

definition (in mut_m) reachable :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
  "reachable y = (❙∃x. root x ❙∧ x reaches y)"

definition grey_reachable :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
  "grey_reachable y = (❙∃g. grey g ❙∧ g reaches y)"


subsection‹ Sundry detritus ›

lemmas eq_imp_simps = ―‹equations for deriving useful things from @{const ‹eq_imp›} facts›
  eq_imp_def
  all_conj_distrib
  split_paired_All split_def fst_conv snd_conv prod_eq_iff
  conj_explode
  simp_thms

lemma p_not_sys:
  "p ≠ sys ⟷ p = gc ∨ (∃m. p = mutator m)"
by (cases p) simp_all

lemma (in mut_m') m'm[iff]: "m' ≠ m"
using mm' by blast

text‹ obj at ›

lemma obj_at_cong[cong]:
  "⟦⋀obj. sys_heap s r = Some obj ⟹ P obj = P' obj; r = r'; s = s'⟧
   ⟹ obj_at P r s ⟷ obj_at P' r' s'"
unfolding obj_at_def by (simp cong: option.case_cong)

lemma obj_at_split:
  "Q (obj_at P r s) = ((sys_heap s r = None ⟶ Q False) ∧ (∀obj. sys_heap s r = Some obj ⟶ Q (P obj)))"
by (simp add: obj_at_def split: option.splits)

lemma obj_at_split_asm:
  "Q (obj_at P r s) = (¬ ((sys_heap s r = None ∧ ¬Q False) ∨ (∃obj. sys_heap s r = Some obj ∧ ¬ Q (P obj))))"
by (simp add: obj_at_def split: option.splits)

lemmas obj_at_splits = obj_at_split obj_at_split_asm

lemma obj_at_eq_imp:
  "eq_imp (λ(_::unit) s. map_option P (sys_heap s r))
          (obj_at P r)"
by (simp add: eq_imp_def obj_at_def split: option.splits)

lemmas obj_at_fun_upd[simp] = eq_imp_fun_upd[OF obj_at_eq_imp, simplified eq_imp_simps]

lemma obj_at_simps:
  "obj_at (λobj. P obj ∧ Q obj) r s ⟷ obj_at P r s ∧ obj_at Q r s"
(*  "obj_at (λobj. R) r s ⟷ valid_ref r s ∧ R" looks good but applies to valid_ref *)
by (simp_all split: obj_at_splits)

text‹ obj at field on heap ›

lemma obj_at_field_on_heap_cong[cong]:
  "⟦⋀r' obj. ⟦sys_heap s r = Some obj; obj_fields obj f = Some r'⟧⟹ P r' = P' r'; r = r'; f = f'; s = s'⟧
   ⟹ obj_at_field_on_heap P r f s ⟷ obj_at_field_on_heap P' r' f' s'"
unfolding obj_at_field_on_heap_def by (simp cong: option.case_cong)

lemma obj_at_field_on_heap_split:
  "Q (obj_at_field_on_heap P r f s) ⟷ ((sys_heap s r = None ⟶ Q False)
                                 ∧ (∀obj. sys_heap s r = Some obj ∧ obj_fields obj f = None ⟶ Q True)
                                 ∧ (∀r' obj. sys_heap s r = Some obj ∧ obj_fields obj f = Some r' ⟶ Q (P r')))"
by (simp add: obj_at_field_on_heap_def split: option.splits)

lemma obj_at_field_on_heap_split_asm:
  "Q (obj_at_field_on_heap P r f s) ⟷ (¬ ((sys_heap s r = None ∧ ¬Q False)
                                    ∨ (∃obj. sys_heap s r = Some obj ∧ obj_fields obj f = None ∧ ¬ Q True)
                                    ∨ (∃r' obj. sys_heap s r = Some obj ∧ obj_fields obj f = Some r' ∧ ¬ Q (P r'))))"
by (simp add: obj_at_field_on_heap_def split: option.splits)

lemmas obj_at_field_on_heap_splits = obj_at_field_on_heap_split obj_at_field_on_heap_split_asm

lemma obj_at_field_on_heap_eq_imp:
  "eq_imp (λ(_::unit) s. sys_heap s r)
          (obj_at_field_on_heap P r f)"
by (simp add: eq_imp_def obj_at_field_on_heap_def)

lemmas obj_at_field_on_heap_fun_upd[simp] = eq_imp_fun_upd[OF obj_at_field_on_heap_eq_imp, simplified eq_imp_simps]

lemma obj_at_field_on_heap_imp_valid_ref[elim]:
  "obj_at_field_on_heap P r f s ⟹ valid_ref r s"
  "obj_at_field_on_heap P r f s ⟹ valid_null_ref (Some r) s"
by (auto simp: obj_at_field_on_heap_def valid_null_ref_def split: obj_at_splits option.splits)

lemma obj_at_field_on_heapE[elim]:
  "⟦ obj_at_field_on_heap P r f s; sys_heap s' r = sys_heap s r; ⋀r'. P r' ⟹ P' r' ⟧
       ⟹ obj_at_field_on_heap P' r f s'"
by (simp add: obj_at_field_on_heap_def split: option.splits)

lemma valid_null_ref_eq_imp:
  "eq_imp (λ(_::unit) s. Option.bind r (map_option ⟨True⟩ ∘ sys_heap s))
          (valid_null_ref r)"
by (simp add: eq_imp_def obj_at_def valid_null_ref_def split: option.splits)

lemmas valid_null_ref_fun_upd[simp] = eq_imp_fun_upd[OF valid_null_ref_eq_imp, simplified]

lemma valid_null_ref_simps[simp]:
  "valid_null_ref None s"
  "valid_null_ref (Some r) s ⟷ valid_ref r s"
unfolding valid_null_ref_def by simp_all

text‹Derive simplification rules from ‹case› expressions›

simps_of_case hs_step_simps[simp]: hs_step_def (splits: hs_phase.split)
simps_of_case do_load_action_simps[simp]: fun_cong[OF do_load_action_def[simplified atomize_eq]] (splits: mem_load_action.split)
simps_of_case do_store_action_simps[simp]: fun_cong[OF do_store_action_def[simplified atomize_eq]] (splits: mem_store_action.split)

(* This gives some indication of how much we're cheating on the TSO front. *)
lemma do_store_action_prj_simps[simp]:
  "fM (do_store_action w s) = fl ⟷ (fM s = fl ∧ w ≠ mw_fM (¬fM s)) ∨ w = mw_fM fl"
  "fl = fM (do_store_action w s) ⟷ (fl = fM s ∧ w ≠ mw_fM (¬fM s)) ∨ w = mw_fM fl"
  "fA (do_store_action w s) = fl ⟷ (fA s = fl ∧ w ≠ mw_fA (¬fA s)) ∨ w = mw_fA fl"
  "fl = fA (do_store_action w s) ⟷ (fl = fA s ∧ w ≠ mw_fA (¬fA s)) ∨ w = mw_fA fl"
  "ghost_hs_in_sync (do_store_action w s) = ghost_hs_in_sync s"
  "ghost_hs_phase (do_store_action w s) = ghost_hs_phase s"
  "ghost_honorary_grey (do_store_action w s) = ghost_honorary_grey s"
  "hs_pending (do_store_action w s) = hs_pending s"
  "hs_type (do_store_action w s) = hs_type s"
  "heap (do_store_action w s) r = None ⟷ heap s r = None"
  "mem_lock (do_store_action w s) = mem_lock s"
  "phase (do_store_action w s) = ph ⟷ (phase s = ph ∧ (∀ph'. w ≠ mw_Phase ph') ∨ w = mw_Phase ph)"
  "ph = phase (do_store_action w s) ⟷ (ph = phase s ∧ (∀ph'. w ≠ mw_Phase ph') ∨ w = mw_Phase ph)"
  "W (do_store_action w s) = W s"
by (auto simp: do_store_action_def fun_upd_apply split: mem_store_action.splits obj_at_splits)


text‹ reaches ›

lemma reaches_refl[iff]:
  "(r reaches r) s"
unfolding reaches_def by blast

lemma reaches_step[intro]:
  "⟦(x reaches y) s; (y points_to z) s⟧ ⟹ (x reaches z) s"
  "⟦(y reaches z) s; (x points_to y) s⟧ ⟹ (x reaches z) s"
unfolding reaches_def
 apply (simp add: rtranclp.rtrancl_into_rtrancl)
apply (simp add: converse_rtranclp_into_rtranclp)
done

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

lemma converse_reachesE[consumes 1, case_names base step]:
  assumes "(x reaches z) s"
  assumes "x = z ⟹ P"
  assumes "⋀y. ⟦(x points_to y) s; (y reaches z) s⟧ ⟹ P"
  shows P
using assms unfolding reaches_def by (blast elim: converse_rtranclpE)

lemma reaches_fields: ― ‹Complicated condition takes care of ‹alloc›: collapses no object and object with no fields›
  assumes "(x reaches y) s'"
  assumes "∀r'. ⋃(ran ` obj_fields ` set_option (sys_heap s' r')) = ⋃(ran ` obj_fields ` set_option (sys_heap s r'))"
  shows "(x reaches 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 by blast
qed simp

lemma reaches_eq_imp:
  "eq_imp (λr' s. ⋃(ran ` obj_fields ` set_option (sys_heap s r')))
          (x reaches y)"
unfolding eq_imp_def by (metis reaches_fields)

lemmas reaches_fun_upd[simp] = eq_imp_fun_upd[OF reaches_eq_imp, simplified eq_imp_simps, rule_format]

text‹

Location-specific facts.

›

lemma obj_at_mark_dequeue[simp]:
  "obj_at P r (s(sys := s sys⦇ heap := (sys_heap s)(r' := map_option (obj_mark_update (λ_. fl)) (sys_heap s r')), mem_store_buffers := wb' ⦈))
⟷ obj_at (λobj. (P (if r = r' then obj⦇ obj_mark := fl ⦈ else obj))) r s"
by (clarsimp simp: fun_upd_apply split: obj_at_splits)

lemma obj_at_field_on_heap_mw_simps[simp]:
  "obj_at_field_on_heap P r0 f0
         (s(sys := (s sys)⦇ heap := (sys_heap s)(r := map_option (λobj :: ('field, 'payload, 'ref) object. obj⦇obj_fields := (obj_fields obj)(f := opt_r')⦈) (sys_heap s r)),
                            mem_store_buffers := (mem_store_buffers (s Sys))(p := ws) ⦈))
⟷ ( (r ≠ r0 ∨ f ≠ f0) ∧ obj_at_field_on_heap P r0 f0 s )
   ∨ (r = r0 ∧ f = f0 ∧ valid_ref r s ∧ (case opt_r' of Some r'' ⇒ P r'' | _ ⇒ True))"
  "obj_at_field_on_heap P r f (s(sys := s sys⦇heap := (sys_heap s)(r' := map_option (obj_mark_update (λ_. fl)) (sys_heap s r')), mem_store_buffers := sb'⦈))
⟷ obj_at_field_on_heap P r f s"
by (auto simp: obj_at_field_on_heap_def fun_upd_apply split: option.splits obj_at_splits)

lemma obj_at_field_on_heap_no_pending_stores:
  "⟦ sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref opt_r'; ∀opt_r'. mw_Mutate r f opt_r' ∉ set (sys_mem_store_buffers (mutator m) s); valid_ref r s ⟧
     ⟹ obj_at_field_on_heap (λr. opt_r' = Some r) r f s"
unfolding sys_load_def fold_stores_def
apply clarsimp
apply (rule fold_invariant[where P="λfr. obj_at_field_on_heap (λr'. Option.bind (heap (fr (s sys)) r) (λobj. obj_fields obj f) = Some r') r f s"
                             and Q="λw. w ∈ set (sys_mem_store_buffers (mutator m) s)"])
  apply fastforce
 apply (fastforce simp: obj_at_field_on_heap_def split: option.splits obj_at_splits)
apply (auto simp: do_store_action_def map_option_case fun_upd_apply
           split: obj_at_field_on_heap_splits option.splits obj_at_splits mem_store_action.splits)
done
(*<*)

end

(*>*)