theory CSpace_R

lemma valid_mdb_ctes_maskedAsFull:
  "\<lbrakk>valid_mdb_ctes m;m src = Some (CTE s_cap s_node)\<rbrakk>
   \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE (maskedAsFull s_cap cap) s_node))" apply (clarsimp simp: maskedAsFull_def) apply (intro conjI impI) apply (frule mdb_inv_preserve_updateCap
    [where m = m and slot = src and index = "max_free_index (capBlockSize cap)"]) apply simp apply (drule mdb_inv_preserve_sym) apply (clarsimp simp:valid_mdb_ctes_def modify_map_def) apply (frule mdb_inv_preserve.preserve_stuff,simp) apply (frule mdb_inv_preserve.by_products,simp) apply (rule mdb_inv_preserve.untyped_inc') apply (erule mdb_inv_preserve_sym) apply (clarsimp split:if_split_asm simp: isCap_simps max_free_index_def) apply simp apply (subgoal_tac "m = m(src \<mapsto> CTE s_cap s_node)") apply simp apply (rule ext) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE (maskedAsFull s_cap cap) s_node)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> (isUntypedCap s_cap \<and> isUntypedCap cap \<and> capPtr s_cap = capPtr cap \<and> capBlockSize s_cap = capBlockSize cap \<longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))) \<and> ((capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap) \<longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE s_cap s_node))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); isUntypedCap s_cap \<and> isUntypedCap cap \<and> capPtr s_cap = capPtr cap \<and> capBlockSize s_cap = capBlockSize cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))
 2. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE s_cap s_node)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); isUntypedCap s_cap \<and> isUntypedCap cap \<and> capPtr s_cap = capPtr cap \<and> capBlockSize s_cap = capBlockSize cap\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap (CTE s_cap s_node))
 2. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); isUntypedCap s_cap \<and> isUntypedCap cap \<and> capPtr s_cap = capPtr cap \<and> capBlockSize s_cap = capBlockSize cap; mdb_inv_preserve m (modify_map m src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap (CTE s_cap s_node)))))\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))
 3. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE s_cap s_node)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); isUntypedCap s_cap \<and> isUntypedCap cap \<and> capPtr s_cap = capPtr cap \<and> capBlockSize s_cap = capBlockSize cap; mdb_inv_preserve m (modify_map m src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap (CTE s_cap s_node)))))\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))
 2. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE s_cap s_node)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); isUntypedCap s_cap \<and> isUntypedCap cap \<and> capPtr s_cap = capPtr cap \<and> capBlockSize s_cap = capBlockSize cap; mdb_inv_preserve (modify_map m src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap (CTE s_cap s_node))))) m\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))
 2. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE s_cap s_node)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE s_cap s_node); mdb_inv_preserve (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) m; valid_dlist m; isUntypedCap s_cap; no_0 m; isUntypedCap cap; mdb_chain_0 m; capPtr s_cap = capPtr cap; capBlockSize s_cap = capBlockSize cap; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m\<rbrakk> \<Longrightarrow> valid_dlist (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> no_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chain_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_badges (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> caps_contained' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chunked (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> untyped_mdb' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> untyped_inc' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_nullcaps (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> ut_revocable' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> class_links (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> distinct_zombies (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> irq_control (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> reply_masters_rvk_fb (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))
 2. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE s_cap s_node)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE s_cap s_node); mdb_inv_preserve (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) m; valid_dlist m; isUntypedCap s_cap; no_0 m; isUntypedCap cap; mdb_chain_0 m; capPtr s_cap = capPtr cap; capBlockSize s_cap = capBlockSize cap; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; valid_dlist (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> ut_revocable' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> class_links (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> distinct_zombies (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> caps_contained' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chunked (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_badges (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> untyped_mdb' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> irq_control (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))\<rbrakk> \<Longrightarrow> no_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chain_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> untyped_inc' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_nullcaps (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> reply_masters_rvk_fb (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))
 2. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE s_cap s_node)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE s_cap s_node); mdb_inv_preserve (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) m; valid_dlist m; isUntypedCap s_cap; no_0 m; isUntypedCap cap; mdb_chain_0 m; capPtr s_cap = capPtr cap; capBlockSize s_cap = capBlockSize cap; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; valid_dlist (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> ut_revocable' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> class_links (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> distinct_zombies (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> caps_contained' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chunked (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_badges (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> untyped_mdb' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> irq_control (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)); reply_masters_rvk_fb (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> no_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chain_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_nullcaps (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))\<rbrakk> \<Longrightarrow> untyped_inc' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))
 2. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE s_cap s_node)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m src = Some (CTE s_cap s_node); mdb_inv_preserve (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) m; valid_dlist m; isUntypedCap s_cap; no_0 m; isUntypedCap cap; mdb_chain_0 m; capPtr s_cap = capPtr cap; capBlockSize s_cap = capBlockSize cap; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; valid_dlist (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> ut_revocable' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> class_links (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> distinct_zombies (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> caps_contained' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chunked (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_badges (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> untyped_mdb' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> irq_control (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)); reply_masters_rvk_fb (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> no_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chain_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_nullcaps (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))\<rbrakk> \<Longrightarrow> mdb_inv_preserve ?m40 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))
 2. \<And>x cte cte'. \<lbrakk>m src = Some (CTE s_cap s_node); mdb_inv_preserve (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) m; valid_dlist m; isUntypedCap s_cap; no_0 m; isUntypedCap cap; mdb_chain_0 m; capPtr s_cap = capPtr cap; capBlockSize s_cap = capBlockSize cap; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; valid_dlist (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> ut_revocable' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> class_links (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> distinct_zombies (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> caps_contained' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chunked (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_badges (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> untyped_mdb' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> irq_control (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)); reply_masters_rvk_fb (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> no_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chain_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_nullcaps (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)); ?m40 x = Some cte; (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) x = Some cte'; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte') \<subseteq> usableUntypedRange (cteCap cte)
 3. \<lbrakk>m src = Some (CTE s_cap s_node); mdb_inv_preserve (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) m; valid_dlist m; isUntypedCap s_cap; no_0 m; isUntypedCap cap; mdb_chain_0 m; capPtr s_cap = capPtr cap; capBlockSize s_cap = capBlockSize cap; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; valid_dlist (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> ut_revocable' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> class_links (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> distinct_zombies (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> caps_contained' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chunked (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_badges (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> untyped_mdb' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> irq_control (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)); reply_masters_rvk_fb (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> no_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chain_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_nullcaps (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))\<rbrakk> \<Longrightarrow> untyped_inc' ?m40
 4. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE s_cap s_node)) proof (prove)
goal (3 subgoals):
 1. \<And>x cte cte'. \<lbrakk>m src = Some (CTE s_cap s_node); mdb_inv_preserve (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) m; valid_dlist m; isUntypedCap s_cap; no_0 m; isUntypedCap cap; mdb_chain_0 m; capPtr s_cap = capPtr cap; capBlockSize s_cap = capBlockSize cap; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; valid_dlist (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> ut_revocable' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> class_links (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> distinct_zombies (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> caps_contained' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chunked (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_badges (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> untyped_mdb' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> irq_control (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)); reply_masters_rvk_fb (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> no_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chain_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_nullcaps (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)); m x = Some cte; (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) x = Some cte'; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte') \<subseteq> usableUntypedRange (cteCap cte)
 2. \<lbrakk>m src = Some (CTE s_cap s_node); mdb_inv_preserve (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) m; valid_dlist m; isUntypedCap s_cap; no_0 m; isUntypedCap cap; mdb_chain_0 m; capPtr s_cap = capPtr cap; capBlockSize s_cap = capBlockSize cap; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; valid_dlist (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> ut_revocable' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> class_links (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> distinct_zombies (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> caps_contained' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chunked (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_badges (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> untyped_mdb' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> irq_control (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)); reply_masters_rvk_fb (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> no_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chain_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_nullcaps (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))\<rbrakk> \<Longrightarrow> untyped_inc' m
 3. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE s_cap s_node)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE s_cap s_node); mdb_inv_preserve (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) m; valid_dlist m; isUntypedCap s_cap; no_0 m; isUntypedCap cap; mdb_chain_0 m; capPtr s_cap = capPtr cap; capBlockSize s_cap = capBlockSize cap; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; valid_dlist (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> ut_revocable' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> class_links (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> distinct_zombies (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> caps_contained' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chunked (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_badges (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> untyped_mdb' (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> irq_control (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)); reply_masters_rvk_fb (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> no_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> mdb_chain_0 (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node)) \<and> valid_nullcaps (m(src \<mapsto> CTE (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) s_cap) s_node))\<rbrakk> \<Longrightarrow> untyped_inc' m
 2. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE s_cap s_node)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE s_cap s_node)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap; m = m(src \<mapsto> CTE s_cap s_node)\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(src \<mapsto> CTE s_cap s_node))
 2. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> m = m(src \<mapsto> CTE s_cap s_node) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> m = m(src \<mapsto> CTE s_cap s_node) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_mdb_ctes m; m src = Some (CTE s_cap s_node); capPtr s_cap = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap s_cap \<longrightarrow> capBlockSize s_cap \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> m x = (m(src \<mapsto> CTE s_cap s_node)) x proof (prove)
goal:
No subgoals!