Theory Valid_Refs

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

(*>*)
section‹ Valid refs inv proofs ›

lemma valid_refs_inv_sweep_loop_free:
  assumes "valid_refs_inv s"
  assumes ngr: "no_grey_refs s"
  assumes rsi: "∀m'. mut_m.reachable_snapshot_inv m' s"
  assumes "white r' s"
  shows "valid_refs_inv (s(sys := s sys⦇heap := (sys_heap s)(r' := None)⦈))"
using assms unfolding valid_refs_inv_def grey_reachable_def no_grey_refs_def
apply (clarsimp dest!: reachable_sweep_loop_free)
apply (drule mut_m.reachable_blackD[OF ngr spec[OF rsi]])
apply (auto split: obj_at_splits)
done

lemma (in gc) valid_refs_inv[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ fM_fA_invL ❙∧ handshake_invL ❙∧ gc_W_empty_invL ❙∧ gc_mark.mark_object_invL ❙∧ obj_fields_marked_invL ❙∧ phase_invL ❙∧ sweep_loop_invL
       ❙∧ LSTP (handshake_phase_inv ❙∧ mutators_phase_inv ❙∧ sys_phase_inv ❙∧ valid_refs_inv ❙∧ valid_W_inv) ⦄
     gc
   ⦃ LSTP valid_refs_inv ⦄"
proof(vcg_jackhammer (no_thin_post_inv), vcg_name_cases)
     case (sweep_loop_free s s') then show ?case
apply -
apply (drule (1) handshake_in_syncD)
apply (rule valid_refs_inv_sweep_loop_free, assumption, assumption)
 apply (simp; fail)
apply (simp add: white_def) (* FIXME rule? *)
done
qed (auto simp: valid_refs_inv_def grey_reachable_def)

context mut_m
begin

lemma valid_refs_inv_discard_roots:
  "⟦ valid_refs_inv s; roots' ⊆ mut_roots s ⟧
     ⟹ valid_refs_inv (s(mutator m := s (mutator m)⦇roots := roots'⦈))"
unfolding valid_refs_inv_def mut_m.reachable_def by (auto simp: fun_upd_apply)

lemma valid_refs_inv_load:
  "⟦ valid_refs_inv s; sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref r'; r ∈ mut_roots s ⟧
     ⟹ valid_refs_inv (s(mutator m := s (mutator m)⦇roots := mut_roots s ∪ Option.set_option r'⦈))"
unfolding valid_refs_inv_def by (simp add: fun_upd_apply)

lemma valid_refs_inv_alloc:
  "⟦ valid_refs_inv s; sys_heap s r' = None ⟧
     ⟹ valid_refs_inv (s(mutator m := s (mutator m)⦇roots := insert r' (mut_roots s)⦈, sys := s sys⦇heap := (sys_heap s)(r' ↦ ⦇obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty⦈)⦈))"
unfolding valid_refs_inv_def mut_m.reachable_def
apply (clarsimp simp: fun_upd_apply)
apply (auto elim: converse_reachesE split: obj_at_splits)
done

lemma valid_refs_inv_store_ins:
  "⟦ valid_refs_inv s; r ∈ mut_roots s; (∃r'. opt_r' = Some r') ⟶ the opt_r' ∈ mut_roots s ⟧
     ⟹ valid_refs_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']) ⦈))"
apply (subst valid_refs_inv_def)
apply (auto simp: grey_reachable_def mut_m.reachable_def fun_upd_apply)
(* FIXME what's gone wrong here? *)
apply (subst (asm) tso_store_refs_simps; force)+
done

lemma valid_refs_inv_deref_del:
  "⟦ valid_refs_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 = {} ⟧
     ⟹ valid_refs_inv (s(mutator m := s (mutator m)⦇ghost_honorary_root := Option.set_option opt_r', ref := opt_r'⦈))"
unfolding valid_refs_inv_def by (simp add: fun_upd_apply)

lemma valid_refs_inv_mo_co_mark:
  "⟦ r ∈ mut_roots s ∪ mut_ghost_honorary_root s; mut_ghost_honorary_grey s = {}; valid_refs_inv s ⟧
     ⟹ valid_refs_inv (s(mutator m := s (mutator m)⦇ghost_honorary_grey := {r}⦈))"
unfolding valid_refs_inv_def
apply (clarsimp simp: grey_reachable_def fun_upd_apply)
apply (metis grey_reachable_def valid_refs_invD(1) valid_refs_invD(10) valid_refs_inv_def)
done

lemma valid_refs_inv[intro]:
  notes fun_upd_apply[simp]
  notes valid_refs_inv_discard_roots[simp]
  notes valid_refs_inv_load[simp]
  notes valid_refs_inv_alloc[simp]
  notes valid_refs_inv_store_ins[simp]
  notes valid_refs_inv_deref_del[simp]
  notes valid_refs_inv_mo_co_mark[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 valid_refs_inv ⦄
     mutator m
   ⦃ LSTP valid_refs_inv ⦄"
proof(vcg_jackhammer (keep_locs) (no_thin_post_inv), vcg_name_cases)
next case (hs_get_roots_done s s') then show ?case by (clarsimp simp: valid_refs_inv_def grey_reachable_def)
next case (hs_get_work_done s s') then show ?case by (clarsimp simp: valid_refs_inv_def grey_reachable_def)
qed

end

lemma (in sys) valid_refs_inv[intro]:
  "⦃ LSTP (valid_refs_inv ❙∧ tso_store_inv) ⦄ sys ⦃ LSTP valid_refs_inv ⦄"
proof(vcg_jackhammer (no_thin_post_inv), vcg_name_cases)
  case (tso_dequeue_store_buffer s s' p w ws) then show ?case
    unfolding do_store_action_def
    apply (auto simp: p_not_sys valid_refs_inv_dequeue_Mutate valid_refs_inv_dequeue_Mutate_Payload fun_upd_apply split: mem_store_action.splits)
    done
qed

(*<*)

end
(*>*)