theory Frame_SD

lemma sep_map_f_tcb_at:
  "\<lbrakk><ptr \<mapsto>f tcb \<and>* R> s ; is_tcb tcb\<rbrakk>
  \<Longrightarrow> tcb_at'
  (\<lambda>t. object_clean (object_wipe_slots (Tcb t)) = object_clean (object_wipe_slots tcb))
  ptr s" apply (simp add:sep_state_projection_def) apply (clarsimp simp:sep_map_f_conj
    object_project_def is_tcb_def
    split:option.splits cdl_object.splits) apply (rename_tac cdl_tcb z) apply (case_tac z,
         simp_all add: object_wipe_slots_def object_clean_def asid_reset_def
                       update_slots_def intent_reset_def) apply (simp add: object_at_def object_slots_def object_wipe_slots_def
                   update_slots_def) apply (rename_tac cdl_tcb') apply (case_tac cdl_tcb) apply (case_tac cdl_tcb') apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl.lift (ptr \<mapsto>f tcb \<and>* R) s; is_tcb tcb\<rbrakk> \<Longrightarrow> tcb_at' (\<lambda>tcba. object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots tcb)) ptr s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ptr \<mapsto>f tcb \<and>* R) (SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq))); is_tcb tcb\<rbrakk> \<Longrightarrow> tcb_at' (\<lambda>tcba. object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots tcb)) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>x3 z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((ptr, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); tcb = Tcb x3; cdl_objects s ptr = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean (Tcb x3))\<rbrakk> \<Longrightarrow> tcb_at' (\<lambda>tcb. object_clean (object_wipe_slots (Tcb tcb)) = object_clean (object_wipe_slots (Tcb x3))) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>cdl_tcb z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((ptr, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); tcb = Tcb cdl_tcb; cdl_objects s ptr = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean (Tcb cdl_tcb))\<rbrakk> \<Longrightarrow> tcb_at' (\<lambda>tcb. object_clean (object_wipe_slots (Tcb tcb)) = object_clean (object_wipe_slots (Tcb cdl_tcb))) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>cdl_tcb z x3. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((ptr, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); tcb = Tcb cdl_tcb; cdl_objects s ptr = Some (Tcb x3); x3\<lparr>cdl_tcb_intent := undefined, cdl_tcb_caps := \<lambda>x. None\<rparr> = cdl_tcb\<lparr>cdl_tcb_intent := undefined, cdl_tcb_caps := \<lambda>x. None\<rparr>; z = Tcb x3\<rbrakk> \<Longrightarrow> tcb_at' (\<lambda>tcb. tcb\<lparr>cdl_tcb_caps := reset_cap_asid o_M object_slots (Tcb (tcb\<lparr>cdl_tcb_caps := \<lambda>x. None\<rparr>)), cdl_tcb_intent := undefined\<rparr> = cdl_tcb\<lparr>cdl_tcb_caps := reset_cap_asid o_M object_slots (Tcb (cdl_tcb\<lparr>cdl_tcb_caps := \<lambda>x. None\<rparr>)), cdl_tcb_intent := undefined\<rparr>) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>cdl_tcb z x3. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((ptr, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); tcb = Tcb cdl_tcb; cdl_objects s ptr = Some (Tcb x3); x3\<lparr>cdl_tcb_intent := undefined, cdl_tcb_caps := \<lambda>x. None\<rparr> = cdl_tcb\<lparr>cdl_tcb_intent := undefined, cdl_tcb_caps := \<lambda>x. None\<rparr>; z = Tcb x3\<rbrakk> \<Longrightarrow> x3\<lparr>cdl_tcb_caps := \<lambda>x. None, cdl_tcb_intent := undefined\<rparr> = cdl_tcb\<lparr>cdl_tcb_caps := \<lambda>x. None, cdl_tcb_intent := undefined\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>cdl_tcb z cdl_tcb'. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((ptr, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); tcb = Tcb cdl_tcb; cdl_objects s ptr = Some (Tcb cdl_tcb'); cdl_tcb'\<lparr>cdl_tcb_intent := undefined, cdl_tcb_caps := \<lambda>x. None\<rparr> = cdl_tcb\<lparr>cdl_tcb_intent := undefined, cdl_tcb_caps := \<lambda>x. None\<rparr>; z = Tcb cdl_tcb'\<rbrakk> \<Longrightarrow> cdl_tcb'\<lparr>cdl_tcb_caps := \<lambda>x. None, cdl_tcb_intent := undefined\<rparr> = cdl_tcb\<lparr>cdl_tcb_caps := \<lambda>x. None, cdl_tcb_intent := undefined\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>cdl_tcb z cdl_tcb' cdl_tcb_caps cdl_tcb_fault_endpoint cdl_tcb_intent cdl_tcb_has_fault cdl_tcb_domain. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((ptr, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); tcb = Tcb cdl_tcb; cdl_objects s ptr = Some (Tcb cdl_tcb'); cdl_tcb'\<lparr>cdl_tcb_intent := undefined, cdl_tcb_caps := \<lambda>x. None\<rparr> = cdl_tcb\<lparr>cdl_tcb_intent := undefined, cdl_tcb_caps := \<lambda>x. None\<rparr>; z = Tcb cdl_tcb'; cdl_tcb = \<lparr>cdl_tcb_caps = cdl_tcb_caps, cdl_tcb_fault_endpoint = cdl_tcb_fault_endpoint, cdl_tcb_intent = cdl_tcb_intent, cdl_tcb_has_fault = cdl_tcb_has_fault, cdl_tcb_domain = cdl_tcb_domain\<rparr>\<rbrakk> \<Longrightarrow> cdl_tcb'\<lparr>cdl_tcb_caps := \<lambda>x. None, cdl_tcb_intent := undefined\<rparr> = cdl_tcb\<lparr>cdl_tcb_caps := \<lambda>x. None, cdl_tcb_intent := undefined\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>cdl_tcb z cdl_tcb' cdl_tcb_caps cdl_tcb_fault_endpoint cdl_tcb_intent cdl_tcb_has_fault cdl_tcb_domain cdl_tcb_capsa cdl_tcb_fault_endpointa cdl_tcb_intenta cdl_tcb_has_faulta cdl_tcb_domaina. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((ptr, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); tcb = Tcb cdl_tcb; cdl_objects s ptr = Some (Tcb cdl_tcb'); cdl_tcb'\<lparr>cdl_tcb_intent := undefined, cdl_tcb_caps := \<lambda>x. None\<rparr> = cdl_tcb\<lparr>cdl_tcb_intent := undefined, cdl_tcb_caps := \<lambda>x. None\<rparr>; z = Tcb cdl_tcb'; cdl_tcb = \<lparr>cdl_tcb_caps = cdl_tcb_caps, cdl_tcb_fault_endpoint = cdl_tcb_fault_endpoint, cdl_tcb_intent = cdl_tcb_intent, cdl_tcb_has_fault = cdl_tcb_has_fault, cdl_tcb_domain = cdl_tcb_domain\<rparr>; cdl_tcb' = \<lparr>cdl_tcb_caps = cdl_tcb_capsa, cdl_tcb_fault_endpoint = cdl_tcb_fault_endpointa, cdl_tcb_intent = cdl_tcb_intenta, cdl_tcb_has_fault = cdl_tcb_has_faulta, cdl_tcb_domain = cdl_tcb_domaina\<rparr>\<rbrakk> \<Longrightarrow> cdl_tcb'\<lparr>cdl_tcb_caps := \<lambda>x. None, cdl_tcb_intent := undefined\<rparr> = cdl_tcb\<lparr>cdl_tcb_caps := \<lambda>x. None, cdl_tcb_intent := undefined\<rparr> proof (prove)
goal:
No subgoals!