theory Frame_SD

lemma sep_map_c_conj:
  "(ptr \<mapsto>c cap \<and>* R) s =
  (let slot = (fst ptr,Slot (snd ptr))
  in (sep_heap s) slot  = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and>
     R (SepState ((sep_heap s)(slot:= None)) (sep_irq_node s)))" apply (clarsimp simp:sep_conj_def Let_def plus_sep_state_def sep_state_add_def) apply (rule iffI) apply (clarsimp simp:sep_map_c_def sep_disj_sep_state_def
     sep_map_general_def sep_state_disj_def map_disj_def) apply (subst object_to_sep_state_add) apply (simp add:dom_object_to_sep_state singleton_iff)+ apply (simp add:object_project_def object_slots_object_clean) apply (erule arg_cong[where f = R,THEN iffD1,rotated]) apply (case_tac y) apply simp apply (rule ext) apply (clarsimp simp: dom_def map_add_def object_to_sep_state_def
                   split: if_split_asm option.splits) apply (clarsimp simp:sep_map_c_def) apply (rule_tac x = "SepState [(fst ptr,Slot (snd ptr))\<mapsto> (CDL_Cap (Some (reset_cap_asid cap)))]
                                Map.empty" in exI) apply (rule_tac x = "(SepState ((sep_heap s)((fst ptr,Slot (snd ptr)):= None)))
                                 (sep_irq_node s) " in exI) apply (clarsimp simp: sep_map_c_def sep_disj_sep_state_def
                        sep_map_general_def sep_state_disj_def map_disj_def) apply (intro conjI) apply (case_tac s,simp) apply (rule ext) apply (clarsimp simp:map_add_def split:option.splits) apply (clarsimp simp:object_to_sep_state_def split:if_splits) apply (rule_tac x = "CNode \<lparr>cdl_cnode_caps = [slot\<mapsto> cap],
    cdl_cnode_size_bits = of_nat slot\<rparr>" in exI) apply (clarsimp simp:object_slots_def) apply (rule ext) apply (clarsimp simp:object_project_def object_slots_def
    object_clean_def asid_reset_def update_slots_def
    intent_reset_def split:if_splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ptr \<mapsto>c cap \<and>* R) s = (let slot = (fst ptr, Slot (snd ptr)) in sep_heap s slot = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((sep_heap s)(slot := None)) (sep_irq_node s))) proof (prove)
goal (1 subgoal):
 1. (\<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>c cap) x \<and> R y) = (sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s))) proof (prove)
goal (2 subgoals):
 1. \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>c cap) x \<and> R y \<Longrightarrow> sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s))
 2. sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>c cap) x \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya obj. \<lbrakk>dom (object_to_sep_state xa obj {Slot ya}) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state xa obj {Slot ya} ++ sep_heap y) (sep_irq_node y); R y; ptr = (xa, ya); sep_heap x = object_to_sep_state xa obj {Slot ya}; sep_irq_node x = (\<lambda>x. None); object_slots obj = [ya \<mapsto> cap]\<rbrakk> \<Longrightarrow> (object_to_sep_state xa obj {Slot ya} ++ sep_heap y) (xa, Slot ya) = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((object_to_sep_state xa obj {Slot ya} ++ sep_heap y)((xa, Slot ya) := None)) (sep_irq_node y))
 2. sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>c cap) x \<and> R y proof (prove)
goal (4 subgoals):
 1. \<And>x y xa ya obj. \<lbrakk>dom (object_to_sep_state xa obj {Slot ya}) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state xa obj {Slot ya} ++ sep_heap y) (sep_irq_node y); R y; ptr = (xa, ya); sep_heap x = object_to_sep_state xa obj {Slot ya}; sep_irq_node x = (\<lambda>x. None); object_slots obj = [ya \<mapsto> cap]\<rbrakk> \<Longrightarrow> {xa} \<times> {Slot ya} \<inter> dom (sep_heap y) = {}
 2. \<And>x y xa ya obj. \<lbrakk>dom (object_to_sep_state xa obj {Slot ya}) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state xa obj {Slot ya} ++ sep_heap y) (sep_irq_node y); R y; ptr = (xa, ya); sep_heap x = object_to_sep_state xa obj {Slot ya}; sep_irq_node x = (\<lambda>x. None); object_slots obj = [ya \<mapsto> cap]\<rbrakk> \<Longrightarrow> Slot ya \<in> {Slot ya}
 3. \<And>x y xa ya obj. \<lbrakk>dom (object_to_sep_state xa obj {Slot ya}) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state xa obj {Slot ya} ++ sep_heap y) (sep_irq_node y); R y; ptr = (xa, ya); sep_heap x = object_to_sep_state xa obj {Slot ya}; sep_irq_node x = (\<lambda>x. None); object_slots obj = [ya \<mapsto> cap]\<rbrakk> \<Longrightarrow> Some (object_project (Slot ya) obj) = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((object_to_sep_state xa obj {Slot ya} ++ sep_heap y)((xa, Slot ya) := None)) (sep_irq_node y))
 4. sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>c cap) x \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya obj. \<lbrakk>(xa, Slot ya) \<notin> dom (sep_heap y); s = SepState (object_to_sep_state xa obj {Slot ya} ++ sep_heap y) (sep_irq_node y); R y; ptr = (xa, ya); sep_heap x = object_to_sep_state xa obj {Slot ya}; sep_irq_node x = (\<lambda>x. None); object_slots obj = [ya \<mapsto> cap]\<rbrakk> \<Longrightarrow> object_project (Slot ya) obj = CDL_Cap (Some (reset_cap_asid cap)) \<and> R (SepState ((object_to_sep_state xa obj {Slot ya} ++ sep_heap y)((xa, Slot ya) := None)) (sep_irq_node y))
 2. sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>c cap) x \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya obj. \<lbrakk>(xa, Slot ya) \<notin> dom (sep_heap y); s = SepState (object_to_sep_state xa obj {Slot ya} ++ sep_heap y) (sep_irq_node y); R y; ptr = (xa, ya); sep_heap x = object_to_sep_state xa obj {Slot ya}; sep_irq_node x = (\<lambda>x. None); object_slots obj = [ya \<mapsto> cap]\<rbrakk> \<Longrightarrow> R (SepState ((object_to_sep_state xa obj {Slot ya} ++ sep_heap y)((xa, Slot ya) := None)) (sep_irq_node y))
 2. sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>c cap) x \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya obj. \<lbrakk>(xa, Slot ya) \<notin> dom (sep_heap y); s = SepState (object_to_sep_state xa obj {Slot ya} ++ sep_heap y) (sep_irq_node y); ptr = (xa, ya); sep_heap x = object_to_sep_state xa obj {Slot ya}; sep_irq_node x = (\<lambda>x. None); object_slots obj = [ya \<mapsto> cap]\<rbrakk> \<Longrightarrow> y = SepState ((object_to_sep_state xa obj {Slot ya} ++ sep_heap y)((xa, Slot ya) := None)) (sep_irq_node y)
 2. sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>c cap) x \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya obj x1 x2. \<lbrakk>(xa, Slot ya) \<notin> dom (sep_heap y); s = SepState (object_to_sep_state xa obj {Slot ya} ++ sep_heap y) (sep_irq_node y); ptr = (xa, ya); sep_heap x = object_to_sep_state xa obj {Slot ya}; sep_irq_node x = (\<lambda>x. None); object_slots obj = [ya \<mapsto> cap]; y = SepState x1 x2\<rbrakk> \<Longrightarrow> y = SepState ((object_to_sep_state xa obj {Slot ya} ++ sep_heap y)((xa, Slot ya) := None)) (sep_irq_node y)
 2. sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>c cap) x \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya obj x1 x2. \<lbrakk>(xa, Slot ya) \<notin> dom x1; s = SepState (object_to_sep_state xa obj {Slot ya} ++ x1) x2; ptr = (xa, ya); sep_heap x = object_to_sep_state xa obj {Slot ya}; sep_irq_node x = (\<lambda>x. None); object_slots obj = [ya \<mapsto> cap]; y = SepState x1 x2\<rbrakk> \<Longrightarrow> x1 = (object_to_sep_state xa obj {Slot ya} ++ x1)((xa, Slot ya) := None)
 2. sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>c cap) x \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya obj x1 x2 xb. \<lbrakk>(xa, Slot ya) \<notin> dom x1; s = SepState (object_to_sep_state xa obj {Slot ya} ++ x1) x2; ptr = (xa, ya); sep_heap x = object_to_sep_state xa obj {Slot ya}; sep_irq_node x = (\<lambda>x. None); object_slots obj = [ya \<mapsto> cap]; y = SepState x1 x2\<rbrakk> \<Longrightarrow> x1 xb = ((object_to_sep_state xa obj {Slot ya} ++ x1)((xa, Slot ya) := None)) xb
 2. sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>c cap) x \<and> R y proof (prove)
goal (1 subgoal):
 1. sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))) \<and> R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>c cap) x \<and> R y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (case ptr of (obj_id, slot) \<Rightarrow> \<exists>obj. sep_map_general obj_id obj {Slot slot} x \<and> object_slots obj = [slot \<mapsto> cap]) \<and> R y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> \<exists>y. SepState [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] (\<lambda>x. None) ## y \<and> s = SepState (sep_heap (SepState [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] (\<lambda>x. None)) ++ sep_heap y) (sep_irq_node (SepState [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] (\<lambda>x. None)) ++ sep_irq_node y) \<and> (case ptr of (obj_id, slot) \<Rightarrow> \<exists>obj. sep_map_general obj_id obj {Slot slot} (SepState [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] (\<lambda>x. None)) \<and> object_slots obj = [slot \<mapsto> cap]) \<and> R y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> SepState [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] (\<lambda>x. None) ## SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s) \<and> s = SepState (sep_heap (SepState [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] (\<lambda>x. None)) ++ sep_heap (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s))) (sep_irq_node (SepState [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] (\<lambda>x. None)) ++ sep_irq_node (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s))) \<and> (case ptr of (obj_id, slot) \<Rightarrow> \<exists>obj. sep_map_general obj_id obj {Slot slot} (SepState [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] (\<lambda>x. None)) \<and> object_slots obj = [slot \<mapsto> cap]) \<and> R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> s = SepState ([(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] ++ (sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s) \<and> (case ptr of (obj_id, slot) \<Rightarrow> \<exists>obj. [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] = object_to_sep_state obj_id obj {Slot slot} \<and> object_slots obj = [slot \<mapsto> cap]) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> s = SepState ([(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] ++ (sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s)
 2. \<lbrakk>sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> case ptr of (obj_id, slot) \<Rightarrow> \<exists>obj. [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] = object_to_sep_state obj_id obj {Slot slot} \<and> object_slots obj = [slot \<mapsto> cap] proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>x1 (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState (x1((fst ptr, Slot (snd ptr)) := None)) x2); s = SepState x1 x2\<rbrakk> \<Longrightarrow> x1 = [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] ++ x1((fst ptr, Slot (snd ptr)) := None)
 2. \<lbrakk>sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> case ptr of (obj_id, slot) \<Rightarrow> \<exists>obj. [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] = object_to_sep_state obj_id obj {Slot slot} \<and> object_slots obj = [slot \<mapsto> cap] proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x. \<lbrakk>x1 (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState (x1((fst ptr, Slot (snd ptr)) := None)) x2); s = SepState x1 x2\<rbrakk> \<Longrightarrow> x1 x = ([(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] ++ x1((fst ptr, Slot (snd ptr)) := None)) x
 2. \<lbrakk>sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> case ptr of (obj_id, slot) \<Rightarrow> \<exists>obj. [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] = object_to_sep_state obj_id obj {Slot slot} \<and> object_slots obj = [slot \<mapsto> cap] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap s (fst ptr, Slot (snd ptr)) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState ((sep_heap s)((fst ptr, Slot (snd ptr)) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> case ptr of (obj_id, slot) \<Rightarrow> \<exists>obj. [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] = object_to_sep_state obj_id obj {Slot slot} \<and> object_slots obj = [slot \<mapsto> cap] proof (prove)
goal (1 subgoal):
 1. \<And>obj_id slot. \<lbrakk>sep_heap s (obj_id, Slot slot) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState ((sep_heap s)((obj_id, Slot slot) := None)) (sep_irq_node s)); ptr = (obj_id, slot)\<rbrakk> \<Longrightarrow> \<exists>obj. [(obj_id, Slot slot) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id obj) else None) \<and> object_slots obj = [slot \<mapsto> cap] proof (prove)
goal (1 subgoal):
 1. \<And>obj_id slot. \<lbrakk>sep_heap s (obj_id, Slot slot) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState ((sep_heap s)((obj_id, Slot slot) := None)) (sep_irq_node s)); ptr = (obj_id, slot)\<rbrakk> \<Longrightarrow> [(obj_id, Slot slot) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id (CNode \<lparr>cdl_cnode_caps = [slot \<mapsto> cap], cdl_cnode_size_bits = of_nat slot\<rparr>)) else None) \<and> object_slots (CNode \<lparr>cdl_cnode_caps = [slot \<mapsto> cap], cdl_cnode_size_bits = of_nat slot\<rparr>) = [slot \<mapsto> cap] proof (prove)
goal (1 subgoal):
 1. \<And>obj_id slot. \<lbrakk>sep_heap s (obj_id, Slot slot) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState ((sep_heap s)((obj_id, Slot slot) := None)) (sep_irq_node s)); ptr = (obj_id, slot)\<rbrakk> \<Longrightarrow> [(obj_id, Slot slot) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id (CNode \<lparr>cdl_cnode_caps = [slot \<mapsto> cap], cdl_cnode_size_bits = of_nat slot\<rparr>)) else None) proof (prove)
goal (1 subgoal):
 1. \<And>obj_id slot x. \<lbrakk>sep_heap s (obj_id, Slot slot) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState ((sep_heap s)((obj_id, Slot slot) := None)) (sep_irq_node s)); ptr = (obj_id, slot)\<rbrakk> \<Longrightarrow> [(obj_id, Slot slot) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] x = (case x of (obj_id', comp_id) \<Rightarrow> if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id (CNode \<lparr>cdl_cnode_caps = [slot \<mapsto> cap], cdl_cnode_size_bits = of_nat slot\<rparr>)) else None) proof (prove)
goal:
No subgoals!