theory CSpace_R

lemma setUntypedCapAsFull_safe_parent_for':
  "\<lbrace>\<lambda>s. safe_parent_for' (ctes_of s) slot a \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrace>
   setUntypedCapAsFull (cteCap srcCTE) c' slot
   \<lbrace>\<lambda>rv s. safe_parent_for' (ctes_of s) slot a\<rbrace>" apply (clarsimp simp:safe_parent_for'_def setUntypedCapAsFull_def split:if_splits) apply (intro conjI impI) apply (wp updateCap_ctes_of_wp) apply (subgoal_tac "mdb_inv_preserve (ctes_of s)
     (modify_map (ctes_of s) slot
     (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))))") apply (frule mdb_inv_preserve.descendants_of[where p = slot]) apply (clarsimp simp:isCap_simps modify_map_def cte_wp_at_ctes_of simp del:fun_upd_apply) apply (clarsimp cong:sameRegionAs_update_untyped) apply (rule mdb_inv_preserve_updateCap) apply (simp add:cte_wp_at_ctes_of) apply simp apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. safe_parent_for' (ctes_of s) slot a \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrace> setUntypedCapAsFull (cteCap srcCTE) c' slot \<lbrace>\<lambda>rv s. safe_parent_for' (ctes_of s) slot a\<rbrace> proof (prove)
goal (1 subgoal):
 1. (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c' \<longrightarrow> \<lbrace>\<lambda>s. (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) \<lbrace>\<lambda>rv s. \<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)\<rbrace>) \<and> ((capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c') \<longrightarrow> \<lbrace>\<lambda>s. (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrace> return () \<lbrace>\<lambda>rv s. \<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)\<rbrace>) proof (prove)
goal (2 subgoals):
 1. isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c' \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) \<lbrace>\<lambda>rv s. \<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)\<rbrace>
 2. capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c' \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrace> return () \<lbrace>\<lambda>rv s. \<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'; (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrakk> \<Longrightarrow> \<exists>parent. (\<exists>node. modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)))) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)
 2. capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c' \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrace> return () \<lbrace>\<lambda>rv s. \<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'; (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s; mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))))\<rbrakk> \<Longrightarrow> \<exists>parent. (\<exists>node. modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)))) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)
 2. \<And>s. \<lbrakk>isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'; (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrakk> \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))))
 3. capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c' \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrace> return () \<lbrace>\<lambda>rv s. \<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'; (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s; mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)))); descendants_of' slot (ctes_of s) = descendants_of' slot (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))))\<rbrakk> \<Longrightarrow> \<exists>parent. (\<exists>node. modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)))) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)
 2. \<And>s. \<lbrakk>isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'; (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrakk> \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))))
 3. capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c' \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrace> return () \<lbrace>\<lambda>rv s. \<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s d f da v0a v1a fa node. \<lbrakk>mdb_inv_preserve (ctes_of s) ((ctes_of s)(slot \<mapsto> CTE (capability.UntypedCap d v0a v1a (max_free_index v1a)) node)); descendants_of' slot (ctes_of s) = {}; c' = capability.UntypedCap da v0a v1a fa; ctes_of s slot = Some (CTE (capability.UntypedCap d v0a v1a f) node); global.sameRegionAs (capability.UntypedCap d v0a v1a f) a; srcCTE = CTE (capability.UntypedCap d v0a v1a f) node; descendants_of' slot ((ctes_of s)(slot \<mapsto> CTE (capability.UntypedCap d v0a v1a (max_free_index v1a)) node)) = {}; capRange a \<noteq> {}; capBits a \<le> v1a\<rbrakk> \<Longrightarrow> \<exists>parent. (\<exists>nodea. ((ctes_of s)(slot \<mapsto> CTE (capability.UntypedCap d v0a v1a (max_free_index v1a)) node)) slot = Some (CTE parent nodea)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ((ctes_of s)(slot \<mapsto> CTE (capability.UntypedCap d v0a v1a (max_free_index v1a)) node)) p \<noteq> Some (CTE a n')) \<or> (\<exists>d v0 v1 f. parent = capability.UntypedCap d v0 v1 f) \<and> capBits a \<le> capBits parent)
 2. \<And>s. \<lbrakk>isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'; (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrakk> \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))))
 3. capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c' \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrace> return () \<lbrace>\<lambda>rv s. \<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'; (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrakk> \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))))
 2. capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c' \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrace> return () \<lbrace>\<lambda>rv s. \<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'; (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrakk> \<Longrightarrow> ctes_of s slot = Some srcCTE
 2. \<And>s. \<lbrakk>isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'; (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap srcCTE)
 3. capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c' \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrace> return () \<lbrace>\<lambda>rv s. \<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'; (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap srcCTE)
 2. capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c' \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrace> return () \<lbrace>\<lambda>rv s. \<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)\<rbrace> proof (prove)
goal (1 subgoal):
 1. capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c' \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrace> return () \<lbrace>\<lambda>rv s. \<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'; (\<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent)) \<and> cte_wp_at' ((=) srcCTE) slot s\<rbrakk> \<Longrightarrow> \<exists>parent. (\<exists>node. ctes_of s slot = Some (CTE parent node)) \<and> global.sameRegionAs parent a \<and> ((\<exists>irq. a = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. ctes_of s p \<noteq> Some (CTE a n')) \<or> isUntypedCap parent \<and> descendants_of' slot (ctes_of s) = {} \<and> capRange a \<noteq> {} \<and> capBits a \<le> capBits parent) proof (prove)
goal:
No subgoals!