theory Retype_C

lemma insertNewCap_descendants_range_in':
  "\<lbrace>\<lambda>s. valid_pspace' s \<and> descendants_range_in' S p (ctes_of s)
    \<and> capRange x \<inter> S = {}
    \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> sameRegionAs (cteCap cte) x) p s
    \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dslot s
    \<and> descendants_range' x p (ctes_of s) \<and> capClass x = PhysicalClass
   \<rbrace> insertNewCap p dslot x
    \<lbrace>\<lambda>rv s. descendants_range_in' S p (ctes_of s)\<rbrace>" apply (clarsimp simp:insertNewCap_def descendants_range_in'_def) apply (wp getCTE_wp) apply (clarsimp simp:cte_wp_at_ctes_of) apply (intro conjI allI) apply (clarsimp simp:valid_pspace'_def valid_mdb'_def
     valid_mdb_ctes_def no_0_def split:if_splits) apply (clarsimp simp: descendants_of'_mdbPrev split:if_splits) apply (cut_tac p = p and m = "ctes_of s" and parent = p and s = s
        and parent_cap = "cteCap cte" and parent_node = "cteMDBNode cte"
        and site = dslot and site_cap = capability.NullCap and site_node = "cteMDBNode ctea"
        and c' = x
    in mdb_insert_again_child.descendants) apply (case_tac cte ,case_tac ctea) apply (rule mdb_insert_again_child.intro[OF mdb_insert_again.intro]) apply (simp add:mdb_ptr_def vmdb_def valid_pspace'_def valid_mdb'_def
            mdb_ptr_axioms_def mdb_insert_again_axioms_def )+ apply (intro conjI allI impI) apply clarsimp apply (erule(1) ctes_of_valid_cap') apply (clarsimp simp:valid_mdb_ctes_def) apply clarsimp apply (rule mdb_insert_again_child_axioms.intro) apply (clarsimp simp: nullPointer_def)+ apply (clarsimp simp:isMDBParentOf_def valid_pspace'_def
      valid_mdb'_def valid_mdb_ctes_def) apply (frule(2) ut_revocableD'[rotated 1]) apply (clarsimp simp:isCap_simps) apply (clarsimp cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace' s \<and> descendants_range_in' S p (ctes_of s) \<and> capRange x \<inter> S = {} \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) x) p s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dslot s \<and> descendants_range' x p (ctes_of s) \<and> capClass x = PhysicalClass\<rbrace> insertNewCap p dslot x \<lbrace>\<lambda>rv s. descendants_range_in' S p (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace' s \<and> (\<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}) \<and> capRange x \<inter> S = {} \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) x) p s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dslot s \<and> descendants_range' x p (ctes_of s) \<and> capClass x = PhysicalClass\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE p);
oldCTE <- getCTE dslot;
y <- assert (nullCapPointers oldCTE);
y <- setCTE dslot (CTE x (MDB next p True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. dslot));
y <- updateMDB p (mdbNext_update (\<lambda>_. dslot));
updateNewFreeIndex dslot
od \<lbrace>\<lambda>rv s. \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_pspace' s \<and> (\<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}) \<and> capRange x \<inter> S = {} \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) x) p s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dslot s \<and> descendants_range' x p (ctes_of s) \<and> capClass x = PhysicalClass \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p s \<and> ((\<lambda>next s. cte_wp_at' (\<lambda>_. True) dslot s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) dslot s \<and> (nullCapPointers cte \<longrightarrow> no_0 ((ctes_of s)(dslot \<mapsto> CTE x (MDB next p True True))) \<and> no_0 ((ctes_of s)(dslot \<mapsto> CTE x (MDB next p True True))) \<and> (\<forall>p'\<in>descendants_of' p (modify_map (modify_map ((ctes_of s)(dslot \<mapsto> CTE x (MDB next p True True))) next (cteMDBNode_update (mdbPrev_update (\<lambda>_. dslot)))) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))). \<forall>c. (\<exists>n. modify_map (modify_map ((ctes_of s)(dslot \<mapsto> CTE x (MDB next p True True))) next (cteMDBNode_update (mdbPrev_update (\<lambda>_. dslot)))) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot))) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {})))) \<circ> (mdbNext \<circ> cteMDBNode)) cte s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) \<and> (\<forall>p'\<in>descendants_of' p (modify_map (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dslot)))). \<forall>c. (\<exists>n. (if p' = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s p') = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a)
 2. \<And>s cte ctea. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer\<rbrakk> \<Longrightarrow> \<forall>p'\<in>descendants_of' p (modify_map (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dslot)))). \<forall>c. (\<exists>n. (if p' = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s p') = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer\<rbrakk> \<Longrightarrow> \<forall>p'\<in>descendants_of' p (modify_map (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dslot)))). \<forall>c. (\<exists>n. (if p' = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s p') = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n)\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n)\<rbrakk> \<Longrightarrow> mdb_insert_again_child (ctes_of s) p (cteCap cte) (cteMDBNode cte) dslot capability.NullCap (cteMDBNode ctea) x s
 2. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); descendants_of' p (modify_map (\<lambda>xa. if xa = dslot then Some (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True)) else ctes_of s xa) p (cteMDBNode_update (mdbNext_update (\<lambda>x. dslot)))) = (if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {dslot} else descendants_of' p (ctes_of s))\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_insert_again_child (ctes_of s) p (cteCap cte) (cteMDBNode cte) dslot capability.NullCap (cteMDBNode ctea) x s
 2. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); descendants_of' p (modify_map (\<lambda>xa. if xa = dslot then Some (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True)) else ctes_of s xa) p (cteMDBNode_update (mdbNext_update (\<lambda>x. dslot)))) = (if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {dslot} else descendants_of' p (ctes_of s))\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (5 subgoals):
 1. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_ptr (ctes_of s) p (cteCap cte) (cteMDBNode cte)
 2. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_ptr (ctes_of s) dslot capability.NullCap (cteMDBNode ctea)
 3. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_insert_again_axioms (ctes_of s) p (cteCap cte) dslot capability.NullCap (cteMDBNode ctea) x s
 4. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_insert_again_child_axioms p (cteCap cte) (cteMDBNode cte) x
 5. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); descendants_of' p (modify_map (\<lambda>xa. if xa = dslot then Some (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True)) else ctes_of s xa) p (cteMDBNode_update (mdbNext_update (\<lambda>x. dslot)))) = (if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {dslot} else descendants_of' p (ctes_of s))\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s); \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some (CTE capability.NullCap x2a); x1a = capability.NullCap; isUntypedCap x1; global.sameRegionAs x1 x; ctes_of s p = Some (CTE x1 x2); mdbNext x2a = nullPointer; mdbPrev x2a = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE capability.NullCap x2a\<rbrakk> \<Longrightarrow> (\<forall>p cap. (\<exists>node. ctes_of s p = Some (CTE cap node)) \<longrightarrow> valid_cap' cap s) \<and> ut_revocable' (ctes_of s) \<and> p \<noteq> dslot
 2. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_insert_again_child_axioms p (cteCap cte) (cteMDBNode cte) x
 3. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); descendants_of' p (modify_map (\<lambda>xa. if xa = dslot then Some (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True)) else ctes_of s xa) p (cteMDBNode_update (mdbNext_update (\<lambda>x. dslot)))) = (if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {dslot} else descendants_of' p (ctes_of s))\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (5 subgoals):
 1. \<And>s cte ctea p' c n x1 x2 x1a x2a pa cap. \<lbrakk>valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s); \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some (CTE capability.NullCap x2a); x1a = capability.NullCap; isUntypedCap x1; global.sameRegionAs x1 x; ctes_of s p = Some (CTE x1 x2); mdbNext x2a = nullPointer; mdbPrev x2a = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE capability.NullCap x2a; \<exists>node. ctes_of s pa = Some (CTE cap node)\<rbrakk> \<Longrightarrow> valid_cap' cap s
 2. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s); \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some (CTE capability.NullCap x2a); x1a = capability.NullCap; isUntypedCap x1; global.sameRegionAs x1 x; ctes_of s p = Some (CTE x1 x2); mdbNext x2a = nullPointer; mdbPrev x2a = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE capability.NullCap x2a\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 3. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s); \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some (CTE capability.NullCap x2a); x1a = capability.NullCap; isUntypedCap x1; global.sameRegionAs x1 x; ctes_of s p = Some (CTE x1 x2); mdbNext x2a = nullPointer; mdbPrev x2a = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE capability.NullCap x2a\<rbrakk> \<Longrightarrow> p \<noteq> dslot
 4. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_insert_again_child_axioms p (cteCap cte) (cteMDBNode cte) x
 5. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); descendants_of' p (modify_map (\<lambda>xa. if xa = dslot then Some (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True)) else ctes_of s xa) p (cteMDBNode_update (mdbNext_update (\<lambda>x. dslot)))) = (if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {dslot} else descendants_of' p (ctes_of s))\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (5 subgoals):
 1. \<And>s p' c n x1 x2 x2a pa cap node. \<lbrakk>\<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some (CTE capability.NullCap x2a); isUntypedCap x1; global.sameRegionAs x1 x; ctes_of s p = Some (CTE x1 x2); mdbNext x2a = nullPointer; mdbPrev x2a = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) (CTE x1 x2)) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); ctes_of s pa = Some (CTE cap node); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s)\<rbrakk> \<Longrightarrow> valid_cap' cap s
 2. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s); \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some (CTE capability.NullCap x2a); x1a = capability.NullCap; isUntypedCap x1; global.sameRegionAs x1 x; ctes_of s p = Some (CTE x1 x2); mdbNext x2a = nullPointer; mdbPrev x2a = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE capability.NullCap x2a\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 3. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s); \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some (CTE capability.NullCap x2a); x1a = capability.NullCap; isUntypedCap x1; global.sameRegionAs x1 x; ctes_of s p = Some (CTE x1 x2); mdbNext x2a = nullPointer; mdbPrev x2a = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE capability.NullCap x2a\<rbrakk> \<Longrightarrow> p \<noteq> dslot
 4. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_insert_again_child_axioms p (cteCap cte) (cteMDBNode cte) x
 5. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); descendants_of' p (modify_map (\<lambda>xa. if xa = dslot then Some (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True)) else ctes_of s xa) p (cteMDBNode_update (mdbNext_update (\<lambda>x. dslot)))) = (if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {dslot} else descendants_of' p (ctes_of s))\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s); \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some (CTE capability.NullCap x2a); x1a = capability.NullCap; isUntypedCap x1; global.sameRegionAs x1 x; ctes_of s p = Some (CTE x1 x2); mdbNext x2a = nullPointer; mdbPrev x2a = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE capability.NullCap x2a\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 2. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s); \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some (CTE capability.NullCap x2a); x1a = capability.NullCap; isUntypedCap x1; global.sameRegionAs x1 x; ctes_of s p = Some (CTE x1 x2); mdbNext x2a = nullPointer; mdbPrev x2a = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE capability.NullCap x2a\<rbrakk> \<Longrightarrow> p \<noteq> dslot
 3. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_insert_again_child_axioms p (cteCap cte) (cteMDBNode cte) x
 4. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); descendants_of' p (modify_map (\<lambda>xa. if xa = dslot then Some (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True)) else ctes_of s xa) p (cteMDBNode_update (mdbNext_update (\<lambda>x. dslot)))) = (if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {dslot} else descendants_of' p (ctes_of s))\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s); \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some (CTE capability.NullCap x2a); x1a = capability.NullCap; isUntypedCap x1; global.sameRegionAs x1 x; ctes_of s p = Some (CTE x1 x2); mdbNext x2a = nullPointer; mdbPrev x2a = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE capability.NullCap x2a\<rbrakk> \<Longrightarrow> p \<noteq> dslot
 2. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_insert_again_child_axioms p (cteCap cte) (cteMDBNode cte) x
 3. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); descendants_of' p (modify_map (\<lambda>xa. if xa = dslot then Some (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True)) else ctes_of s xa) p (cteMDBNode_update (mdbNext_update (\<lambda>x. dslot)))) = (if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {dslot} else descendants_of' p (ctes_of s))\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_insert_again_child_axioms p (cteCap cte) (cteMDBNode cte) x
 2. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); descendants_of' p (modify_map (\<lambda>xa. if xa = dslot then Some (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True)) else ctes_of s xa) p (cteMDBNode_update (mdbNext_update (\<lambda>x. dslot)))) = (if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {dslot} else descendants_of' p (ctes_of s))\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea p' c n x1 x2 x1a x2a. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE (cteCap cte) (cteMDBNode cte)) (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True))
 2. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); descendants_of' p (modify_map (\<lambda>xa. if xa = dslot then Some (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True)) else ctes_of s xa) p (cteMDBNode_update (mdbNext_update (\<lambda>x. dslot)))) = (if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {dslot} else descendants_of' p (ctes_of s))\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s p' c n x1 x2 x2a. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some (CTE capability.NullCap x2a); isUntypedCap x1; global.sameRegionAs x1 x; ctes_of s p = Some (CTE x1 x2); mdbNext x2a = 0; mdbPrev x2a = 0; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) (CTE x1 x2)) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n)\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1 x2) (CTE x (MDB (mdbNext x2) p True True))
 2. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); descendants_of' p (modify_map (\<lambda>xa. if xa = dslot then Some (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True)) else ctes_of s xa) p (cteMDBNode_update (mdbNext_update (\<lambda>x. dslot)))) = (if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {dslot} else descendants_of' p (ctes_of s))\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s p' c n x1 x2 x2a. \<lbrakk>\<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some (CTE capability.NullCap x2a); isUntypedCap x1; global.sameRegionAs x1 x; ctes_of s p = Some (CTE x1 x2); mdbNext x2a = 0; mdbPrev x2a = 0; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) (CTE x1 x2)) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> if \<not> mdbRevocable x2 then False else if Not $ x1 `~global.sameRegionAs~` x then False else if True then if isEndpointCap x1 \<and> capEPBadge x1 \<noteq> 0 then let badge = capEPBadge x1 in badge = capEPBadge x \<and> (Not $ mdbFirstBadged (MDB (mdbNext x2) p True True)) else if isNotificationCap x1 \<and> capNtfnBadge x1 \<noteq> 0 then let badge = capNtfnBadge x1 in badge = capNtfnBadge x \<and> (Not $ mdbFirstBadged (MDB (mdbNext x2) p True True)) else True else undefined
 2. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); descendants_of' p (modify_map (\<lambda>xa. if xa = dslot then Some (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True)) else ctes_of s xa) p (cteMDBNode_update (mdbNext_update (\<lambda>x. dslot)))) = (if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {dslot} else descendants_of' p (ctes_of s))\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s p' c n x1 x2 x2a. \<lbrakk>\<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some (CTE capability.NullCap x2a); isUntypedCap x1; global.sameRegionAs x1 x; ctes_of s p = Some (CTE x1 x2); mdbNext x2a = 0; mdbPrev x2a = 0; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) (CTE x1 x2)) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); mdbRevocable x2\<rbrakk> \<Longrightarrow> if \<not> mdbRevocable x2 then False else if Not $ x1 `~global.sameRegionAs~` x then False else if True then if isEndpointCap x1 \<and> capEPBadge x1 \<noteq> 0 then let badge = capEPBadge x1 in badge = capEPBadge x \<and> (Not $ mdbFirstBadged (MDB (mdbNext x2) p True True)) else if isNotificationCap x1 \<and> capNtfnBadge x1 \<noteq> 0 then let badge = capNtfnBadge x1 in badge = capNtfnBadge x \<and> (Not $ mdbFirstBadged (MDB (mdbNext x2) p True True)) else True else undefined
 2. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); descendants_of' p (modify_map (\<lambda>xa. if xa = dslot then Some (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True)) else ctes_of s xa) p (cteMDBNode_update (mdbNext_update (\<lambda>x. dslot)))) = (if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {dslot} else descendants_of' p (ctes_of s))\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea p' c n. \<lbrakk>valid_pspace' s; \<forall>p'\<in>descendants_of' p (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; capRange x \<inter> S = {}; descendants_range' x p (ctes_of s); capClass x = PhysicalClass; ctes_of s dslot = Some ctea; cteCap ctea = capability.NullCap; isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) x; ctes_of s p = Some cte; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; p' \<in> descendants_of' p (modify_map (\<lambda>a. if a = dslot then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) cte) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. dslot)))); p' \<noteq> dslot; ctes_of s p' = Some (CTE c n); descendants_of' p (modify_map (\<lambda>xa. if xa = dslot then Some (CTE x (MDB (mdbNext (cteMDBNode cte)) p True True)) else ctes_of s xa) p (cteMDBNode_update (mdbNext_update (\<lambda>x. dslot)))) = (if p \<in> descendants_of' p (ctes_of s) \<or> p = p then descendants_of' p (ctes_of s) \<union> {dslot} else descendants_of' p (ctes_of s))\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal:
No subgoals!