Theory StrongTricolour

(*<*)
(*
 * 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 StrongTricolour
imports
  Global_Invariants_Lemmas
  Local_Invariants_Lemmas
  Tactics
begin

(*>*)

(* local lemma bucket *)

context mut_m
begin

(* marked insertions *)

lemma marked_insertions_store_ins[simp]:
  "⟦ marked_insertions s; (∃r'. opt_r' = Some r') ⟶ marked (the opt_r') s ⟧
     ⟹ marked_insertions
               (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'])⦈))"
by (auto simp: marked_insertions_def
        split: mem_store_action.splits option.splits)

lemma marked_insertions_alloc[simp]:
  "⟦ heap (s sys) r' = None; valid_refs_inv s ⟧
  ⟹ marked_insertions (s(mutator m' := s (mutator m')⦇roots := roots'⦈, sys := s sys⦇heap := (sys_heap s)(r' ↦ obj')⦈))
  ⟷ marked_insertions s"
apply (clarsimp simp: marked_insertions_def split: mem_store_action.splits option.splits)
apply (rule iffI)
 apply clarsimp
 apply (rename_tac ref field x)
 apply (drule_tac x=ref in spec, drule_tac x=field in spec, drule_tac x=x in spec, clarsimp)
 apply (drule valid_refs_invD(6)[where x=r' and y=r'], simp_all)
done


(* marked_deletions *)

lemma marked_deletions_store_ins[simp]:
  "⟦ marked_deletions s; obj_at_field_on_heap (λr'. marked r' s) r f s ⟧
     ⟹ marked_deletions
               (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'])⦈))"
by (auto simp: marked_deletions_def
        split: mem_store_action.splits option.splits)

lemma marked_deletions_alloc[simp]:
  "⟦ marked_deletions s; heap (s sys) r' = None; valid_refs_inv s ⟧
  ⟹ marked_deletions (s(mutator m' := s (mutator m')⦇roots := roots'⦈, sys := s sys⦇heap := (sys_heap s)(r' ↦ obj')⦈))"
apply (clarsimp simp: marked_deletions_def split: mem_store_action.splits)
apply (rename_tac ref field option)
apply (drule_tac x="mw_Mutate ref field option" in spec)
apply clarsimp
apply (case_tac "ref = r'")
 apply (auto simp: obj_at_field_on_heap_def split: option.splits)
done

end


subsection‹Sweep loop invariants›

lemma (in gc) sweep_loop_invL_eq_imp:
  "eq_imp (λ(_::unit) s. (AT s gc, s↓ gc, sys_fM s↓, map_option obj_mark ∘ sys_heap s↓))
          sweep_loop_invL"
apply (clarsimp simp: eq_imp_def inv)
apply (rename_tac s s')
apply (subgoal_tac "∀r. valid_ref r s↓ ⟷ valid_ref r s'↓")
 apply (subgoal_tac "∀P r. obj_at (λobj. P (obj_mark obj)) r s↓ ⟷ obj_at (λobj. P (obj_mark obj)) r s'↓")
  apply (frule_tac x="λmark. Some mark = gc_mark s'↓" in spec)
  apply (frule_tac x="λmark. mark = sys_fM s'↓" in spec)
  apply clarsimp
 apply (clarsimp simp: fun_eq_iff split: obj_at_splits)
 apply (rename_tac r)
 apply ( (drule_tac x=r in spec)+, auto)[1]
apply (clarsimp simp: fun_eq_iff split: obj_at_splits)
apply (rename_tac r)
apply (drule_tac x=r in spec, auto)[1]
apply (metis map_option_eq_Some)+
done

lemmas gc_sweep_loop_invL_niE[nie] =
  iffD1[OF gc.sweep_loop_invL_eq_imp[simplified eq_imp_simps, rule_format, unfolded conj_explode, rule_format], rotated -1]

lemma (in gc) sweep_loop_invL[intro]:
  "⦃ fM_fA_invL ❙∧ phase_invL ❙∧ sweep_loop_invL ❙∧ tso_lock_invL
         ❙∧ LSTP (phase_rel_inv ❙∧ mutators_phase_inv ❙∧ valid_W_inv) ⦄
     gc
   ⦃ sweep_loop_invL ⦄"
proof(vcg_jackhammer, vcg_name_cases)
     case sweep_loop_ref_done  then show ?case by blast
next case sweep_loop_check     then show ?case
      apply (clarsimp split: obj_at_splits)
      apply (metis (no_types, lifting) option.collapse option.inject)
      done
next case sweep_loop_load_mark then show ?case by (clarsimp split: obj_at_splits)
qed

context gc
begin

lemma sweep_loop_locs_subseteq_sweep_locs:
  "sweep_loop_locs ⊆ sweep_locs"
by (auto simp: sweep_loop_locs_def sweep_locs_def intro: append_prefixD)

lemma sweep_locs_subseteq_fM_tso_empty_locs:
  "sweep_locs ⊆ fM_tso_empty_locs"
by (auto simp: sweep_locs_def fM_tso_empty_locs_def loc_defs)

lemma sweep_loop_locs_fM_eq_locs:
  "sweep_loop_locs ⊆ fM_eq_locs"
by (auto simp: sweep_loop_locs_def fM_eq_locs_def sweep_locs_def loc_defs)

lemma sweep_loop_locs_fA_eq_locs:
  "sweep_loop_locs ⊆ fA_eq_locs"
apply (simp add: sweep_loop_locs_def fA_eq_locs_def sweep_locs_def)
apply (intro subset_insertI2)
apply (auto intro: append_prefixD)
done

lemma black_heap_locs_subseteq_fM_tso_empty_locs:
  "black_heap_locs ⊆ fM_tso_empty_locs"
by (auto simp: black_heap_locs_def fM_tso_empty_locs_def loc_defs)

lemma black_heap_locs_fM_eq_locs:
  "black_heap_locs ⊆ fM_eq_locs"
by (simp add: black_heap_locs_def fM_eq_locs_def loc_defs)

lemma black_heap_locs_fA_eq_locs:
  "black_heap_locs ⊆ fA_eq_locs"
by (simp add: black_heap_locs_def fA_eq_locs_def sweep_locs_def loc_defs)

lemma fM_fA_invL_tso_emptyD:
  "⟦ atS gc ls s; fM_fA_invL s; ls ⊆ fM_tso_empty_locs ⟧ ⟹ tso_pending_fM gc s↓ = []"
by (auto simp: fM_fA_invL_def dest: atS_mono)

lemma gc_sweep_loop_invL_locsE[rule_format]:
  "(atS gc (sweep_locs ∪ black_heap_locs) s ⟶ False) ⟹ gc.sweep_loop_invL s"
apply (simp add: gc.sweep_loop_invL_def atS_un)
apply (auto simp: locset_cache atS_simps dest: atS_mono)
 apply (simp add: atS_mono gc.sweep_loop_locs_subseteq_sweep_locs; fail)
apply (clarsimp simp: atS_def)
apply (rename_tac x)
apply (drule_tac x=x in bspec)
apply (auto simp: sweep_locs_def sweep_loop_not_choose_ref_locs_def intro: append_prefixD)
done

end

lemma (in sys) gc_sweep_loop_invL[intro]:
  "⦃ gc.fM_fA_invL ❙∧ gc.gc_W_empty_invL ❙∧ gc.sweep_loop_invL
       ❙∧ LSTP (tso_store_inv ❙∧ valid_W_inv) ⦄
     sys
   ⦃ gc.sweep_loop_invL ⦄"
proof(vcg_jackhammer (keep_locs) (no_thin_post_inv), vcg_name_cases)
  case (tso_dequeue_store_buffer s s' p w ws) then show ?case
  proof(cases w)
       case (mw_Mark r fl) with tso_dequeue_store_buffer show ?thesis
        apply -
        apply (rule gc.gc_sweep_loop_invL_locsE)
        apply (simp only: gc.gc_W_empty_invL_def gc.no_grey_refs_locs_def cong del: atS_state_weak_cong)
        apply (clarsimp simp: atS_un)
        apply (thin_tac "AT _ = _") (* FIXME speed the metis call up a bit *)
        apply (thin_tac "at _ _ _ ⟶ _")+
        apply (metis (mono_tags, lifting) filter.simps(2) loc_mem_tac_simps(4) no_grey_refs_no_pending_marks)
        done
  next case (mw_Mutate r f opt_r') with tso_dequeue_store_buffer show ?thesis by clarsimp (erule gc_sweep_loop_invL_niE; simp add: fun_eq_iff fun_upd_apply)
  next case (mw_Mutate_Payload r f pl) with tso_dequeue_store_buffer show ?thesis by clarsimp (erule gc_sweep_loop_invL_niE; simp add: fun_eq_iff fun_upd_apply)
  next case (mw_fA fl) with tso_dequeue_store_buffer show ?thesis by - (erule gc_sweep_loop_invL_niE; simp add: fun_eq_iff)
  next case (mw_fM fl) with tso_dequeue_store_buffer show ?thesis
        apply -
        apply (rule gc.gc_sweep_loop_invL_locsE)
        apply (case_tac p; clarsimp)
        apply (drule (1) gc.fM_fA_invL_tso_emptyD)
        apply simp_all
        using gc.black_heap_locs_subseteq_fM_tso_empty_locs gc.sweep_locs_subseteq_fM_tso_empty_locs apply blast
        done
  next case (mw_Phase ph) with tso_dequeue_store_buffer show ?thesis by - (erule gc_sweep_loop_invL_niE; simp add: fun_eq_iff)
  qed
qed

lemma (in mut_m) gc_sweep_loop_invL[intro]:
  "⦃ gc.fM_fA_invL ❙∧ gc.handshake_invL ❙∧ gc.sweep_loop_invL
       ❙∧ LSTP (mutators_phase_inv ❙∧ valid_refs_inv) ⦄
     mutator m
   ⦃ gc.sweep_loop_invL ⦄"
proof( vcg_chainsaw (no_thin) gc.fM_fA_invL_def gc.sweep_loop_invL_def gc.handshake_invL_def, vcg_name_cases gc)
     case (sweep_loop_locs s s' rb) then show ?case by (metis (no_types, lifting) atS_mono gc.sweep_loop_locs_fA_eq_locs gc.sweep_loop_locs_fM_eq_locs)
next case (black_heap_locs s s' rb) then show ?case by (metis (no_types, lifting) atS_mono gc.black_heap_locs_fA_eq_locs gc.black_heap_locs_fM_eq_locs)
qed


subsection‹ Mutator proofs ›

context mut_m
begin

(* reachable snapshot inv *)

lemma reachable_snapshot_inv_mo_co_mark[simp]:
  "⟦ ghost_honorary_grey (s p) = {}; reachable_snapshot_inv s ⟧
     ⟹ reachable_snapshot_inv (s(p := s p⦇ ghost_honorary_grey := {r} ⦈))"
unfolding in_snapshot_def reachable_snapshot_inv_def by (auto simp: fun_upd_apply)

lemma reachable_snapshot_inv_hs_get_roots_done:
  assumes sti: "strong_tricolour_inv s"
  assumes m: "∀r ∈ mut_roots s. marked r s"
  assumes ghr: "mut_ghost_honorary_root s = {}"
  assumes t: "tso_pending_mutate (mutator m) s = []"
  assumes vri: "valid_refs_inv s"
  shows "reachable_snapshot_inv
               (s(mutator m := s (mutator m)⦇W := {}, ghost_hs_phase := ghp'⦈,
                  sys := s sys⦇hs_pending := hp', W := sys_W s ∪ mut_W s, ghost_hs_in_sync := in'⦈))"
  (is "reachable_snapshot_inv ?s'")
proof(rule, clarsimp)
  fix r assume "reachable r s"
  then show "in_snapshot r ?s'"
  proof (induct rule: reachable_induct)
    case (root x) with m show ?case
      apply (clarsimp simp: in_snapshot_def) (* FIXME intro rules *)
      apply (auto dest: marked_imp_black_or_grey)
      done
  next
    case (ghost_honorary_root x) with ghr show ?case by simp
  next
    case (tso_root x) with t show ?case
      apply (clarsimp simp: filter_empty_conv tso_store_refs_def)
      apply (rename_tac w; case_tac w; fastforce)
      done
  next
    case (reaches x y)
    from reaches vri have "valid_ref x s" "valid_ref y s"
      using reachable_points_to by fastforce+
    with reaches sti vri show ?case
      apply (clarsimp simp: in_snapshot_def)
      apply (elim disjE)
       apply (clarsimp simp: strong_tricolour_inv_def)
       apply (drule spec[where x=x])
       apply clarsimp
       apply (auto dest!: marked_imp_black_or_grey)[1]
      apply (cases "white y s")
      apply (auto dest: grey_protects_whiteE
                 dest!: marked_imp_black_or_grey)
        done
    qed
qed

lemma reachable_snapshot_inv_hs_get_work_done:
  "reachable_snapshot_inv s
    ⟹ reachable_snapshot_inv
               (s(mutator m := s (mutator m)⦇W := {}⦈,
                   sys := s sys⦇hs_pending := pending', W := sys_W s ∪ mut_W s,
                                ghost_hs_in_sync := (ghost_hs_in_sync (s sys))(m := True)⦈))"
by (simp add: reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def)

lemma reachable_snapshot_inv_deref_del:
  "⟦ reachable_snapshot_inv s; sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref opt_r'; r ∈ mut_roots s; mut_ghost_honorary_root s = {} ⟧
     ⟹ reachable_snapshot_inv (s(mutator m := s (mutator m)⦇ghost_honorary_root := Option.set_option opt_r', ref := opt_r'⦈))"
unfolding reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def by (clarsimp simp: fun_upd_apply)

lemma mutator_phase_inv[intro]:
  notes fun_upd_apply[simp]
  notes reachable_snapshot_inv_deref_del[simp]
  notes if_split_asm[split del]
  shows
  "⦃ handshake_invL
       ❙∧ mark_object_invL
       ❙∧ mut_get_roots.mark_object_invL m
       ❙∧ mut_store_del.mark_object_invL m
       ❙∧ mut_store_ins.mark_object_invL m
       ❙∧ LSTP (handshake_phase_inv ❙∧ mutators_phase_inv ❙∧ phase_rel_inv ❙∧ sys_phase_inv ❙∧ fA_rel_inv ❙∧ fM_rel_inv ❙∧ valid_refs_inv ❙∧ strong_tricolour_inv ❙∧ valid_W_inv) ⦄
     mutator m
   ⦃ LSTP mutator_phase_inv ⦄"
proof( vcg_jackhammer (no_thin_post_inv)
    , simp_all add: mutator_phase_inv_aux_case split: hs_phase.splits
    , vcg_name_cases)
     case alloc then show ?case
    apply (drule_tac x=m in spec)
    apply (drule handshake_phase_invD)
    apply (clarsimp simp: fA_rel_inv_def fM_rel_inv_def fM_rel_def hp_step_rel_def split: if_split_asm)
    apply (intro conjI impI; simp)
     apply (elim disjE; force simp: fA_rel_def)
    apply (rule reachable_snapshot_inv_alloc, simp_all)
    apply (elim disjE; force simp: fA_rel_def)
    done
next case (store_ins s s') then show ?case
    apply (drule_tac x=m in spec)
    apply (drule handshake_phase_invD)
    apply (intro conjI impI; clarsimp)
      apply (rule marked_deletions_store_ins, assumption) (* FIXME shuffle the following into this lemma *)
      apply (cases "(∀opt_r'. mw_Mutate (mut_tmp_ref s↓) (mut_field s↓) opt_r' ∉ set (sys_mem_store_buffers (mutator m) s↓))"; clarsimp)
      apply (force simp: marked_deletions_def)
     apply (erule marked_insertions_store_ins)
     apply (drule phase_rel_invD)
     apply (clarsimp simp: phase_rel_def hp_step_rel_def; elim disjE; fastforce dest: reachable_blackD elim: blackD; fail)
    apply (rule marked_deletions_store_ins; clarsimp) (* FIXME as above *)
    apply (erule disjE; clarsimp)
     apply (drule phase_rel_invD)
     apply (clarsimp simp: phase_rel_def)
     apply (elim disjE; clarsimp)
      apply (fastforce simp: hp_step_rel_def)
     apply (clarsimp simp: hp_step_rel_def)
     apply (case_tac "sys_ghost_hs_phase s↓"; clarsimp) (* FIXME invert handshake_phase_rel *)
      apply (clarsimp simp: obj_at_field_on_heap_def split: option.splits)
      apply (rule conjI, fast, clarsimp)
      apply (frule_tac r=x2a in blackD(1)[OF reachable_blackD], simp_all)[1]
      apply (rule_tac x="mut_tmp_ref s↓" in reachable_points_to; auto simp: ran_def split: obj_at_splits; fail)
     apply (clarsimp simp: obj_at_field_on_heap_def split: option.splits)
     apply (rule conjI, fast, clarsimp)
     apply (frule_tac r=x2a in blackD(1)[OF reachable_blackD], simp_all)[1]
     apply (rule_tac x="mut_tmp_ref s↓" in reachable_points_to; auto simp: ran_def split: obj_at_splits; fail)
    apply (force simp: marked_deletions_def)
    done
next case (hs_noop_done s s') then show ?case
    apply -
    apply (drule_tac x=m in spec)
    apply (drule handshake_phase_invD)
    apply (simp add: fA_rel_def fM_rel_def hp_step_rel_def)
    apply (cases "mut_ghost_hs_phase s↓") (* FIXME invert handshake_step *)
    apply auto
    done
next case (hs_get_roots_done s s') then show ?case
    apply -
    apply (drule_tac x=m in spec)
    apply (drule handshake_phase_invD)
    apply (force simp: hp_step_rel_def reachable_snapshot_inv_hs_get_roots_done)
    done
next case (hs_get_work_done s s') then show ?case
    apply (drule_tac x=m in spec)
    apply (drule handshake_phase_invD)
    apply (force simp add: hp_step_rel_def reachable_snapshot_inv_hs_get_work_done)
    done
qed

end

lemma (in mut_m') mutator_phase_inv[intro]:
  notes mut_m.mark_object_invL_def[inv]
  notes mut_m.handshake_invL_def[inv]
  notes fun_upd_apply[simp]
  shows
  "⦃ handshake_invL ❙∧ mut_m.handshake_invL m'
       ❙∧ mut_m.mark_object_invL m'
       ❙∧ mut_get_roots.mark_object_invL m'
       ❙∧ mut_store_del.mark_object_invL m'
       ❙∧ mut_store_ins.mark_object_invL m'
       ❙∧ LSTP (fA_rel_inv ❙∧ fM_rel_inv ❙∧ handshake_phase_inv ❙∧ mutators_phase_inv ❙∧ valid_refs_inv) ⦄
     mutator m'
   ⦃ LSTP mutator_phase_inv ⦄"
proof( vcg_jackhammer (no_thin_post_inv)
    , simp_all add: mutator_phase_inv_aux_case split: hs_phase.splits
    , vcg_name_cases)
     case (alloc s s' rb) then show ?case
      apply -
      apply (clarsimp simp: fA_rel_inv_def fM_rel_inv_def white_def)
      apply (drule spec[where x=m])
      apply (intro conjI impI; clarsimp)
       apply (clarsimp simp: hp_step_rel_def simp: fA_rel_def fM_rel_def dest!: handshake_phase_invD)
       apply (elim disjE, auto; fail)
      apply (rule reachable_snapshot_inv_alloc, simp_all)
      apply (clarsimp simp: hp_step_rel_def simp: fA_rel_def fM_rel_def dest!: handshake_phase_invD)
      apply (cases "sys_ghost_hs_phase s↓"; clarsimp; blast)
      done
next case (hs_get_roots_done s s') then show ?case
      apply -
      apply (drule spec[where x=m])
      apply (simp add: no_black_refs_def reachable_snapshot_inv_def in_snapshot_def)
      done
next case (hs_get_work_done s s') then show ?case
      apply -
      apply (drule spec[where x=m])
      apply (clarsimp simp: no_black_refs_def reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def)
      done
qed

(* FIXME Some of ‹mutator_phase_inv›, the rest in Global Noninterference *)

lemma no_black_refs_sweep_loop_free[simp]:
  "no_black_refs s ⟹ no_black_refs (s(sys := s sys⦇heap := (sys_heap s)(gc_tmp_ref s := None)⦈))"
unfolding no_black_refs_def by simp

lemma no_black_refs_load_W[simp]:
  "⟦ no_black_refs s; gc_W s = {} ⟧
     ⟹ no_black_refs (s(gc := s gc⦇W := sys_W s⦈, sys := s sys⦇W := {}⦈))"
unfolding no_black_refs_def by simp

lemma marked_insertions_sweep_loop_free[simp]:
  "⟦ mut_m.marked_insertions m s; white r s ⟧
     ⟹ mut_m.marked_insertions m (s(sys := (s sys)⦇heap := (heap (s sys))(r := None)⦈))"
unfolding mut_m.marked_insertions_def by (fastforce simp: fun_upd_apply split: mem_store_action.splits obj_at_splits option.splits)

lemma marked_deletions_sweep_loop_free[simp]:
  notes fun_upd_apply[simp]
  shows
  "⟦ mut_m.marked_deletions m s; mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s ⟧
     ⟹ mut_m.marked_deletions m (s(sys := s sys⦇heap := (sys_heap s)(r := None)⦈))"
unfolding mut_m.marked_deletions_def
apply (clarsimp split: mem_store_action.splits)
apply (rename_tac ref field option)
apply (drule_tac x="mw_Mutate ref field option" in spec)
apply (clarsimp simp: obj_at_field_on_heap_def split: option.splits)
 apply (rule conjI)
  apply (clarsimp simp: mut_m.reachable_snapshot_inv_def)
  apply (drule spec[where x=r], clarsimp simp: in_snapshot_def)
  apply (drule mp, auto simp: mut_m.reachable_def mut_m.tso_store_refs_def split: mem_store_action.splits)[1] (* FIXME rule *)
  apply (drule grey_protects_whiteD)
  apply (clarsimp simp: no_grey_refs_def)
 apply (clarsimp; fail)
apply (rule conjI; clarsimp)
apply (rule conjI)
 apply (clarsimp simp: mut_m.reachable_snapshot_inv_def)
 apply (drule spec[where x=r], clarsimp simp: in_snapshot_def)
 apply (drule mp, auto simp: mut_m.reachable_def mut_m.tso_store_refs_def split: mem_store_action.splits)[1] (* FIXME rule *)
 apply (drule grey_protects_whiteD)
 apply (clarsimp simp: no_grey_refs_def)
unfolding white_def apply (clarsimp split: obj_at_splits)
done

context gc
begin

lemma obj_fields_marked_inv_blacken:
  "⟦ gc_field_set s = {}; obj_fields_marked s; (gc_tmp_ref s points_to w) s; white w s ⟧ ⟹ False"
by (simp add: obj_fields_marked_def obj_at_field_on_heap_def ran_def white_def split: option.splits obj_at_splits)

lemma obj_fields_marked_inv_has_white_path_to_blacken:
  "⟦ gc_field_set s = {}; gc_tmp_ref s ∈ gc_W s; (gc_tmp_ref s has_white_path_to w) s; obj_fields_marked s; valid_W_inv s ⟧ ⟹ w = gc_tmp_ref s"
by (metis (mono_tags, lifting) converse_rtranclpE gc.obj_fields_marked_inv_blacken has_white_path_to_def)

lemma mutator_phase_inv[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ fM_fA_invL ❙∧ gc_W_empty_invL ❙∧ handshake_invL ❙∧ obj_fields_marked_invL ❙∧ sweep_loop_invL
       ❙∧ gc_mark.mark_object_invL
       ❙∧ LSTP (handshake_phase_inv ❙∧ mutators_phase_inv ❙∧ valid_refs_inv ❙∧ valid_W_inv) ⦄
     gc
   ⦃ LSTP (mut_m.mutator_phase_inv m) ⦄"
proof( vcg_jackhammer (no_thin_post_inv)
     , simp_all add: mutator_phase_inv_aux_case white_def split: hs_phase.splits
     , vcg_name_cases )
     case (sweep_loop_free s s') then show ?case
       apply (intro allI conjI impI)
        apply (drule mut_m.handshake_phase_invD[where m=m], clarsimp simp: hp_step_rel_def; fail)
       apply (rule mut_m.reachable_snapshot_inv_sweep_loop_free, simp_all add: white_def)
       done
next case (mark_loop_get_work_load_W s s') then show ?case
      apply clarsimp
      apply (drule spec[where x=m])
      apply (clarsimp simp: mut_m.reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def) (* FIXME rule *)
      done
next case (mark_loop_blacken s s') then show ?case
      apply -
      apply (drule spec[where x=m])
      apply clarsimp
      apply (intro allI conjI impI; clarsimp)
       apply (drule mut_m.handshake_phase_invD[where m=m], clarsimp simp: hp_step_rel_def)
      apply (clarsimp simp: mut_m.reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def)
      apply (metis (no_types, opaque_lifting) obj_fields_marked_inv_has_white_path_to_blacken)
      done
next case (mark_loop_mo_co_mark s s' y) then show ?case by (clarsimp simp: handshake_in_syncD mut_m.reachable_snapshot_inv_mo_co_mark)
next case (mark_loop_get_roots_load_W s s') then show ?case
      apply clarsimp
      apply (drule spec[where x=m])
      apply (clarsimp simp: mut_m.reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def) (* FIXME rule *)
      done
qed

end

lemma (in gc) strong_tricolour_inv[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ fM_fA_invL ❙∧ gc_W_empty_invL ❙∧ gc_mark.mark_object_invL ❙∧ obj_fields_marked_invL ❙∧ sweep_loop_invL
       ❙∧ LSTP (strong_tricolour_inv ❙∧ valid_W_inv) ⦄
     gc
   ⦃ LSTP strong_tricolour_inv ⦄"
unfolding strong_tricolour_inv_def
proof(vcg_jackhammer (no_thin_post_inv), vcg_name_cases)
  case (mark_loop_blacken s s' x xa) then show ?case by (fastforce elim!: obj_fields_marked_inv_blacken)
qed

lemma (in mut_m) strong_tricolour[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ mark_object_invL
      ❙∧ mut_get_roots.mark_object_invL m
      ❙∧ mut_store_del.mark_object_invL m
      ❙∧ mut_store_ins.mark_object_invL m
      ❙∧ LSTP (fA_rel_inv ❙∧ fM_rel_inv ❙∧ handshake_phase_inv ❙∧ mutators_phase_inv ❙∧ strong_tricolour_inv ❙∧ sys_phase_inv ❙∧ valid_refs_inv) ⦄
     mutator m
   ⦃ LSTP strong_tricolour_inv ⦄"
unfolding strong_tricolour_inv_def
proof(vcg_jackhammer (no_thin_post_inv), vcg_name_cases)
  case (alloc s s' x xa rb) then show ?case
apply (clarsimp simp: fA_rel_inv_def fM_rel_inv_def)
apply (drule handshake_phase_invD)
apply (drule spec[where x=m])
apply (clarsimp simp: sys_phase_inv_aux_case
               split: hs_phase.splits if_splits)

 apply (blast dest: heap_colours_colours)

 (* FIXME rule? *)
 apply (metis (no_types, lifting) black_def no_black_refsD obj_at_cong option.simps(3))
 apply (metis (no_types, lifting) black_def no_black_refsD obj_at_cong option.distinct(1))

 apply (clarsimp simp: hp_step_rel_def)
 apply (elim disjE; force simp: fA_rel_def fM_rel_def split: obj_at_splits)

 apply (clarsimp simp: hp_step_rel_def)
 apply (elim disjE; force simp: fA_rel_def fM_rel_def split: obj_at_splits)
done
qed

(*<*)

end
(*>*)