theory Untyped_R

lemma insertNewCap_ranges:
  "\<lbrace>\<lambda>s. descendants_range' c p (ctes_of s) \<and>
   descendants_range' cap p (ctes_of s) \<and>
   capRange c \<inter> capRange cap = {} \<and>
   cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and>
                     sameRegionAs (cteCap cte) cap) p s \<and>
   valid_mdb' s \<and> valid_objs' s\<rbrace>
  insertNewCap p slot cap
  \<lbrace>\<lambda>_ s. descendants_range' c p (ctes_of s)\<rbrace>" apply (simp add: insertNewCap_def) apply (wp getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of) apply (rule conjI) apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def) apply (case_tac ctea) apply (case_tac cteb) apply (clarsimp simp: nullPointer_def cong: if_cong) apply (simp (no_asm) add: descendants_range'_def descendants_of'_mdbPrev) apply (subst mdb_insert_again_child.descendants) apply unfold_locales[1] apply (simp add: valid_mdb'_def) apply (assumption|rule refl)+ apply (frule sameRegionAs_classes, clarsimp simp: isCap_simps) apply (erule (1) ctes_of_valid_cap') apply (simp add: valid_mdb'_def valid_mdb_ctes_def) apply clarsimp apply (clarsimp simp: isMDBParentOf_def) apply (clarsimp simp: isCap_simps valid_mdb'_def
                         valid_mdb_ctes_def ut_revocable'_def) apply clarsimp apply (rule context_conjI, blast) apply (clarsimp simp: descendants_range'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. descendants_range' c p (ctes_of s) \<and> descendants_range' cap p (ctes_of s) \<and> capRange c \<inter> capRange cap = {} \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) p s \<and> valid_mdb' s \<and> valid_objs' s\<rbrace> insertNewCap p slot cap \<lbrace>\<lambda>_ s. descendants_range' c p (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. descendants_range' c p (ctes_of s) \<and> descendants_range' cap p (ctes_of s) \<and> capRange c \<inter> capRange cap = {} \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) p s \<and> valid_mdb' s \<and> valid_objs' s\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE p);
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB next p True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB p (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od \<lbrace>\<lambda>_ s. descendants_range' c p (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. descendants_range' c p (ctes_of s) \<and> descendants_range' cap p (ctes_of s) \<and> capRange c \<inter> capRange cap = {} \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) p s \<and> valid_mdb' s \<and> valid_objs' s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) p s \<longrightarrow> ((\<lambda>next s. \<forall>cte. cte_wp_at' ((=) cte) slot s \<longrightarrow> cteCap cte = capability.NullCap \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> mdbPrev (cteMDBNode cte) = nullPointer \<longrightarrow> no_0 ((ctes_of s)(slot \<mapsto> CTE cap (MDB next p True True))) \<and> no_0 ((ctes_of s)(slot \<mapsto> CTE cap (MDB next p True True))) \<and> descendants_range' c p (modify_map (modify_map ((ctes_of s)(slot \<mapsto> CTE cap (MDB next p True True))) next (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot))))) \<circ> (mdbNext \<circ> cteMDBNode)) cte s proof (prove)
goal (1 subgoal):
 1. \<And>s ctea cteb. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap (cteCap ctea); global.sameRegionAs (cteCap ctea) cap; ctes_of s p = Some ctea; ctes_of s slot = Some cteb; cteCap cteb = capability.NullCap; mdbNext (cteMDBNode cteb) = nullPointer; mdbPrev (cteMDBNode cteb) = nullPointer\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = slot then Some (CTE cap (MDB ((mdbNext \<circ> cteMDBNode) ctea) p True True)) else ctes_of s a) \<and> descendants_range' c p (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB ((mdbNext \<circ> cteMDBNode) ctea) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (2 subgoals):
 1. \<And>s ctea cteb. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap (cteCap ctea); global.sameRegionAs (cteCap ctea) cap; ctes_of s p = Some ctea; ctes_of s slot = Some cteb; cteCap cteb = capability.NullCap; mdbNext (cteMDBNode cteb) = nullPointer; mdbPrev (cteMDBNode cteb) = nullPointer\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = slot then Some (CTE cap (MDB ((mdbNext \<circ> cteMDBNode) ctea) p True True)) else ctes_of s a)
 2. \<And>s ctea cteb. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap (cteCap ctea); global.sameRegionAs (cteCap ctea) cap; ctes_of s p = Some ctea; ctes_of s slot = Some cteb; cteCap cteb = capability.NullCap; mdbNext (cteMDBNode cteb) = nullPointer; mdbPrev (cteMDBNode cteb) = nullPointer\<rbrakk> \<Longrightarrow> descendants_range' c p (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB ((mdbNext \<circ> cteMDBNode) ctea) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (1 subgoal):
 1. \<And>s ctea cteb. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap (cteCap ctea); global.sameRegionAs (cteCap ctea) cap; ctes_of s p = Some ctea; ctes_of s slot = Some cteb; cteCap cteb = capability.NullCap; mdbNext (cteMDBNode cteb) = nullPointer; mdbPrev (cteMDBNode cteb) = nullPointer\<rbrakk> \<Longrightarrow> descendants_range' c p (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB ((mdbNext \<circ> cteMDBNode) ctea) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (1 subgoal):
 1. \<And>s ctea cteb x1 x2. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap (cteCap ctea); global.sameRegionAs (cteCap ctea) cap; ctes_of s p = Some ctea; ctes_of s slot = Some cteb; cteCap cteb = capability.NullCap; mdbNext (cteMDBNode cteb) = nullPointer; mdbPrev (cteMDBNode cteb) = nullPointer; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> descendants_range' c p (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB ((mdbNext \<circ> cteMDBNode) ctea) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (1 subgoal):
 1. \<And>s ctea cteb x1 x2 x1a x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap (cteCap ctea); global.sameRegionAs (cteCap ctea) cap; ctes_of s p = Some ctea; ctes_of s slot = Some cteb; cteCap cteb = capability.NullCap; mdbNext (cteMDBNode cteb) = nullPointer; mdbPrev (cteMDBNode cteb) = nullPointer; ctea = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> descendants_range' c p (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB ((mdbNext \<circ> cteMDBNode) ctea) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> descendants_range' c p (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext x2) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext x2) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> \<forall>p'\<in>descendants_of' p (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext x2) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))). (p' = slot \<longrightarrow> capRange cap \<inter> capRange c = {}) \<and> (p' \<noteq> slot \<longrightarrow> (\<forall>ca. (\<exists>n. ctes_of s p' = Some (CTE ca n)) \<longrightarrow> capRange ca \<inter> capRange c = {})) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> mdb_insert_again_child (ctes_of s) p (?parent_cap76 s x1 x2 x2a) x2 slot (?site_cap76 s x1 x2 x2a) (?site_node76 s x1 x2 x2a) cap (?s76 s x1 x2 x2a)
 2. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> \<forall>p'\<in>if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {slot} else descendants_of' p (ctes_of s). (p' = slot \<longrightarrow> capRange cap \<inter> capRange c = {}) \<and> (p' \<noteq> slot \<longrightarrow> (\<forall>ca. (\<exists>n. ctes_of s p' = Some (CTE ca n)) \<longrightarrow> capRange ca \<inter> capRange c = {})) proof (prove)
goal (15 subgoals):
 1. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> valid_mdb_ctes (ctes_of s)
 2. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> ctes_of s p = Some (CTE (?parent_cap76 s x1 x2 x2a) x2)
 3. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> ctes_of s slot = Some (CTE (?site_cap76 s x1 x2 x2a) (?site_node76 s x1 x2 x2a))
 4. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> ?site_cap76 s x1 x2 x2a = capability.NullCap
 5. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> mdbPrev (?site_node76 s x1 x2 x2a) = 0
 6. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> mdbNext (?site_node76 s x1 x2 x2a) = 0
 7. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> isUntypedCap (?parent_cap76 s x1 x2 x2a)
 8. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> global.sameRegionAs (?parent_cap76 s x1 x2 x2a) cap
 9. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> descendants_range' cap p (ctes_of s)
 10. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> capClass cap = PhysicalClass
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> ctes_of s p = Some (CTE (?parent_cap76 s x1 x2 x2a) x2)
 2. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> ctes_of s slot = Some (CTE (?site_cap76 s x1 x2 x2a) (?site_node76 s x1 x2 x2a))
 3. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> ?site_cap76 s x1 x2 x2a = capability.NullCap
 4. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> mdbPrev (?site_node76 s x1 x2 x2a) = 0
 5. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> mdbNext (?site_node76 s x1 x2 x2a) = 0
 6. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> isUntypedCap (?parent_cap76 s x1 x2 x2a)
 7. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> global.sameRegionAs (?parent_cap76 s x1 x2 x2a) cap
 8. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> descendants_range' cap p (ctes_of s)
 9. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> capClass cap = PhysicalClass
 10. \<And>s x1 x2 x2a pa capa node. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0; ctes_of s pa = Some (CTE capa node)\<rbrakk> \<Longrightarrow> valid_cap' capa (?s76 s x1 x2 x2a)
A total of 14 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> capClass cap = PhysicalClass
 2. \<And>s x1 x2 x2a pa capa node. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0; ctes_of s pa = Some (CTE capa node)\<rbrakk> \<Longrightarrow> valid_cap' capa (?s76 s x1 x2 x2a)
 3. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 4. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> p \<noteq> slot
 5. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1 x2) (CTE cap (MDB (mdbNext x2) p True True))
 6. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> \<forall>p'\<in>if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {slot} else descendants_of' p (ctes_of s). (p' = slot \<longrightarrow> capRange cap \<inter> capRange c = {}) \<and> (p' \<noteq> slot \<longrightarrow> (\<forall>ca. (\<exists>n. ctes_of s p' = Some (CTE ca n)) \<longrightarrow> capRange ca \<inter> capRange c = {})) proof (prove)
goal (5 subgoals):
 1. \<And>s x1 x2 x2a pa capa node. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0; ctes_of s pa = Some (CTE capa node)\<rbrakk> \<Longrightarrow> valid_cap' capa (?s76 s x1 x2 x2a)
 2. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 3. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> p \<noteq> slot
 4. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1 x2) (CTE cap (MDB (mdbNext x2) p True True))
 5. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> \<forall>p'\<in>if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {slot} else descendants_of' p (ctes_of s). (p' = slot \<longrightarrow> capRange cap \<inter> capRange c = {}) \<and> (p' \<noteq> slot \<longrightarrow> (\<forall>ca. (\<exists>n. ctes_of s p' = Some (CTE ca n)) \<longrightarrow> capRange ca \<inter> capRange c = {})) proof (prove)
goal (4 subgoals):
 1. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 2. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> p \<noteq> slot
 3. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1 x2) (CTE cap (MDB (mdbNext x2) p True True))
 4. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> \<forall>p'\<in>if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {slot} else descendants_of' p (ctes_of s). (p' = slot \<longrightarrow> capRange cap \<inter> capRange c = {}) \<and> (p' \<noteq> slot \<longrightarrow> (\<forall>ca. (\<exists>n. ctes_of s p' = Some (CTE ca n)) \<longrightarrow> capRange ca \<inter> capRange c = {})) proof (prove)
goal (3 subgoals):
 1. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> p \<noteq> slot
 2. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1 x2) (CTE cap (MDB (mdbNext x2) p True True))
 3. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> \<forall>p'\<in>if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {slot} else descendants_of' p (ctes_of s). (p' = slot \<longrightarrow> capRange cap \<inter> capRange c = {}) \<and> (p' \<noteq> slot \<longrightarrow> (\<forall>ca. (\<exists>n. ctes_of s p' = Some (CTE ca n)) \<longrightarrow> capRange ca \<inter> capRange c = {})) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1 x2) (CTE cap (MDB (mdbNext x2) p True True))
 2. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> \<forall>p'\<in>if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {slot} else descendants_of' p (ctes_of s). (p' = slot \<longrightarrow> capRange cap \<inter> capRange c = {}) \<and> (p' \<noteq> slot \<longrightarrow> (\<forall>ca. (\<exists>n. ctes_of s p' = Some (CTE ca n)) \<longrightarrow> capRange ca \<inter> capRange c = {})) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> (isNotificationCap x1 \<and> capNtfnBadge x1 \<noteq> 0 \<longrightarrow> (isEndpointCap x1 \<longrightarrow> capEPBadge x1 = 0) \<and> isEndpointCap x1 \<and> capEPBadge x1 \<noteq> 0) \<and> ((isNotificationCap x1 \<longrightarrow> capNtfnBadge x1 = 0) \<longrightarrow> (isEndpointCap x1 \<longrightarrow> capEPBadge x1 = 0) \<and> ((isEndpointCap x1 \<longrightarrow> capEPBadge x1 = 0) \<longrightarrow> mdbRevocable x2))
 2. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> \<forall>p'\<in>if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {slot} else descendants_of' p (ctes_of s). (p' = slot \<longrightarrow> capRange cap \<inter> capRange c = {}) \<and> (p' \<noteq> slot \<longrightarrow> (\<forall>ca. (\<exists>n. ctes_of s p' = Some (CTE ca n)) \<longrightarrow> capRange ca \<inter> capRange c = {})) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> \<forall>p'\<in>if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {slot} else descendants_of' p (ctes_of s). (p' = slot \<longrightarrow> capRange cap \<inter> capRange c = {}) \<and> (p' \<noteq> slot \<longrightarrow> (\<forall>ca. (\<exists>n. ctes_of s p' = Some (CTE ca n)) \<longrightarrow> capRange ca \<inter> capRange c = {})) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c = {} \<and> (\<forall>p'\<in>descendants_of' p (ctes_of s). (p' = slot \<longrightarrow> capRange cap \<inter> capRange c = {}) \<and> (p' \<noteq> slot \<longrightarrow> (\<forall>ca. (\<exists>n. ctes_of s p' = Some (CTE ca n)) \<longrightarrow> capRange ca \<inter> capRange c = {}))) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x2a. \<lbrakk>descendants_range' c p (ctes_of s); descendants_range' cap p (ctes_of s); capRange c \<inter> capRange cap = {}; valid_mdb' s; valid_objs' s; isUntypedCap x1; global.sameRegionAs x1 cap; ctes_of s p = Some (CTE x1 x2); ctes_of s slot = Some (CTE capability.NullCap x2a); mdbNext x2a = 0; mdbPrev x2a = 0; capRange cap \<inter> capRange c = {}\<rbrakk> \<Longrightarrow> \<forall>p'\<in>descendants_of' p (ctes_of s). (p' = slot \<longrightarrow> capRange cap \<inter> capRange c = {}) \<and> (p' \<noteq> slot \<longrightarrow> (\<forall>ca. (\<exists>n. ctes_of s p' = Some (CTE ca n)) \<longrightarrow> capRange ca \<inter> capRange c = {})) proof (prove)
goal:
No subgoals!