theory Untyped_R

lemma insertNewCap_valid_mdb:
  "\<lbrace>valid_mdb' and valid_objs' and K (slot \<noteq> p) and
    caps_overlap_reserved' (untypedRange cap) and
    cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and>
                      sameRegionAs (cteCap cte) cap) p and
    K (\<not>isZombie cap) and valid_cap' cap and
    (\<lambda>s. descendants_range' cap p (ctes_of s))\<rbrace>
  insertNewCap p slot cap
  \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>" apply (clarsimp simp: insertNewCap_def valid_mdb'_def) apply (wp getCTE_ctes_of | simp add: o_def)+ apply (clarsimp simp: cte_wp_at_ctes_of) apply (rule conjI) apply (clarsimp simp: no_0_def valid_mdb_ctes_def) apply (case_tac cte) apply (rename_tac p_cap p_node) apply (clarsimp cong: if_cong) apply (case_tac ya) apply (rename_tac node) apply (clarsimp simp: nullPointer_def) apply (rule mdb_insert_again_all.valid_n') apply unfold_locales[1] apply (assumption|rule refl)+ apply (frule sameRegionAs_classes, clarsimp simp: isCap_simps) apply (erule (1) ctes_of_valid_cap') apply (simp add: valid_mdb_ctes_def) apply simp apply (clarsimp simp: isMDBParentOf_CTE) apply (clarsimp simp: isCap_simps valid_mdb_ctes_def ut_revocable'_def) apply assumption apply (drule(1) caps_overlap_reserved'_D) apply simp apply (simp add:Int_ac) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb' and valid_objs' and K (slot \<noteq> p) and caps_overlap_reserved' (untypedRange cap) and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) p and K (\<not> isZombie cap) and valid_cap' cap and (\<lambda>s. descendants_range' cap p (ctes_of s))\<rbrace> insertNewCap p slot cap \<lbrace>\<lambda>rv. valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. valid_mdb_ctes (ctes_of s)) and valid_objs' and (\<lambda>y. slot \<noteq> p) and caps_overlap_reserved' (untypedRange cap) and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) p and (\<lambda>y. \<not> isZombie cap) and valid_cap' cap and (\<lambda>s. descendants_range' cap p (ctes_of 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>rv s. valid_mdb_ctes (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_mdb_ctes (ctes_of s) \<and> valid_objs' s \<and> slot \<noteq> p \<and> caps_overlap_reserved' (untypedRange cap) s \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) p s \<and> \<not> isZombie cap \<and> valid_cap' cap s \<and> descendants_range' cap p (ctes_of s) \<Longrightarrow> (\<exists>y. ctes_of s p = Some y) \<longrightarrow> (\<exists>y. ctes_of s slot = Some y) \<longrightarrow> cteCap (the (ctes_of s slot)) = capability.NullCap \<and> mdbNext (cteMDBNode (the (ctes_of s slot))) = nullPointer \<and> mdbPrev (cteMDBNode (the (ctes_of s slot))) = nullPointer \<longrightarrow> no_0 (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext (cteMDBNode (the (ctes_of s p)))) p True True)) else ctes_of s a) \<and> valid_mdb_ctes (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext (cteMDBNode (the (ctes_of s p)))) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext (cteMDBNode (the (ctes_of s p)))) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ya. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) cap; ctes_of s p = Some cte; ctes_of s slot = Some ya; cteCap ya = capability.NullCap; mdbNext (cteMDBNode ya) = nullPointer; mdbPrev (cteMDBNode ya) = nullPointer\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext (cteMDBNode (the (ctes_of s p)))) p True True)) else ctes_of s a) \<and> valid_mdb_ctes (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext (cteMDBNode (the (ctes_of s p)))) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ya. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) cap; ctes_of s p = Some cte; ctes_of s slot = Some ya; cteCap ya = capability.NullCap; mdbNext (cteMDBNode ya) = nullPointer; mdbPrev (cteMDBNode ya) = nullPointer\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext (cteMDBNode (the (ctes_of s p)))) p True True)) else ctes_of s a)
 2. \<And>s cte ya. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) cap; ctes_of s p = Some cte; ctes_of s slot = Some ya; cteCap ya = capability.NullCap; mdbNext (cteMDBNode ya) = nullPointer; mdbPrev (cteMDBNode ya) = nullPointer\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext (cteMDBNode (the (ctes_of s p)))) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ya. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) cap; ctes_of s p = Some cte; ctes_of s slot = Some ya; cteCap ya = capability.NullCap; mdbNext (cteMDBNode ya) = nullPointer; mdbPrev (cteMDBNode ya) = nullPointer\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext (cteMDBNode (the (ctes_of s p)))) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ya x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) cap; ctes_of s p = Some cte; ctes_of s slot = Some ya; cteCap ya = capability.NullCap; mdbNext (cteMDBNode ya) = nullPointer; mdbPrev (cteMDBNode ya) = nullPointer; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext (cteMDBNode (the (ctes_of s p)))) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ya p_cap p_node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) cap; ctes_of s p = Some cte; ctes_of s slot = Some ya; cteCap ya = capability.NullCap; mdbNext (cteMDBNode ya) = nullPointer; mdbPrev (cteMDBNode ya) = nullPointer; cte = CTE p_cap p_node\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext (cteMDBNode (the (ctes_of s p)))) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (1 subgoal):
 1. \<And>s ya p_cap p_node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some ya; cteCap ya = capability.NullCap; mdbNext (cteMDBNode ya) = nullPointer; mdbPrev (cteMDBNode ya) = nullPointer\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext p_node) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext p_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (1 subgoal):
 1. \<And>s ya p_cap p_node x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some ya; cteCap ya = capability.NullCap; mdbNext (cteMDBNode ya) = nullPointer; mdbPrev (cteMDBNode ya) = nullPointer; ya = CTE x1 x2\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext p_node) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext p_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (1 subgoal):
 1. \<And>s ya p_cap p_node x1 node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some ya; cteCap ya = capability.NullCap; mdbNext (cteMDBNode ya) = nullPointer; mdbPrev (cteMDBNode ya) = nullPointer; ya = CTE x1 node\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext p_node) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext p_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (1 subgoal):
 1. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (\<lambda>a. if a = slot then Some (CTE cap (MDB (mdbNext p_node) p True True)) else ctes_of s a) p (cteMDBNode_update (mdbNext_update (\<lambda>_. slot)))) (mdbNext p_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. slot)))) proof (prove)
goal (2 subgoals):
 1. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> mdb_insert_again_all (ctes_of s) p (?parent_cap82 s p_cap p_node node) p_node slot (?site_cap82 s p_cap p_node node) (?site_node82 s p_cap p_node node) cap (?s82 s p_cap p_node node)
 2. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange (?parent_cap82 s p_cap p_node node) = {} proof (prove)
goal (16 subgoals):
 1. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> valid_mdb_ctes (ctes_of s)
 2. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> ctes_of s p = Some (CTE (?parent_cap82 s p_cap p_node node) p_node)
 3. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> ctes_of s slot = Some (CTE (?site_cap82 s p_cap p_node node) (?site_node82 s p_cap p_node node))
 4. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> ?site_cap82 s p_cap p_node node = capability.NullCap
 5. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> mdbPrev (?site_node82 s p_cap p_node node) = 0
 6. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> mdbNext (?site_node82 s p_cap p_node node) = 0
 7. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> isUntypedCap (?parent_cap82 s p_cap p_node node)
 8. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> global.sameRegionAs (?parent_cap82 s p_cap p_node node) cap
 9. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> descendants_range' cap p (ctes_of s)
 10. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> capClass cap = PhysicalClass
A total of 16 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> capClass cap = PhysicalClass
 2. \<And>s p_cap p_node node pa capa nodea. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0; ctes_of s pa = Some (CTE capa nodea)\<rbrakk> \<Longrightarrow> valid_cap' capa (?s82 s p_cap p_node node)
 3. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 4. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> p \<noteq> slot
 5. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE p_cap p_node) (CTE cap (MDB (mdbNext p_node) p True True))
 6. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> valid_cap' cap (?s82 s p_cap p_node node)
 7. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange p_cap = {} proof (prove)
goal (6 subgoals):
 1. \<And>s p_cap p_node node pa capa nodea. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0; ctes_of s pa = Some (CTE capa nodea)\<rbrakk> \<Longrightarrow> valid_cap' capa (?s82 s p_cap p_node node)
 2. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 3. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> p \<noteq> slot
 4. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE p_cap p_node) (CTE cap (MDB (mdbNext p_node) p True True))
 5. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> valid_cap' cap (?s82 s p_cap p_node node)
 6. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange p_cap = {} proof (prove)
goal (5 subgoals):
 1. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 2. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> p \<noteq> slot
 3. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE p_cap p_node) (CTE cap (MDB (mdbNext p_node) p True True))
 4. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> valid_cap' cap s
 5. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange p_cap = {} proof (prove)
goal (4 subgoals):
 1. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> p \<noteq> slot
 2. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE p_cap p_node) (CTE cap (MDB (mdbNext p_node) p True True))
 3. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> valid_cap' cap s
 4. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange p_cap = {} proof (prove)
goal (3 subgoals):
 1. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE p_cap p_node) (CTE cap (MDB (mdbNext p_node) p True True))
 2. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> valid_cap' cap s
 3. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange p_cap = {} proof (prove)
goal (3 subgoals):
 1. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> mdbRevocable p_node \<and> (capBadge p_cap, capBadge cap) \<in> capBadge_ordering True
 2. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> valid_cap' cap s
 3. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange p_cap = {} proof (prove)
goal (2 subgoals):
 1. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> valid_cap' cap s
 2. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange p_cap = {} proof (prove)
goal (1 subgoal):
 1. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; caps_overlap_reserved' (untypedRange cap) s; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange p_cap = {} proof (prove)
goal (2 subgoals):
 1. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap (CTE p_cap p_node))
 2. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0; usableUntypedRange (cteCap (CTE p_cap p_node)) \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange p_cap = {} proof (prove)
goal (1 subgoal):
 1. \<And>s p_cap p_node node. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; slot \<noteq> p; \<not> isZombie cap; valid_cap' cap s; descendants_range' cap p (ctes_of s); isUntypedCap p_cap; global.sameRegionAs p_cap cap; ctes_of s p = Some (CTE p_cap p_node); ctes_of s slot = Some (CTE capability.NullCap node); mdbNext node = 0; mdbPrev node = 0; usableUntypedRange (cteCap (CTE p_cap p_node)) \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange p_cap = {} proof (prove)
goal:
No subgoals!