theory CSpace1_R

lemma setUntypedCapAsFull_mdb[wp]:
  "\<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' (\<lambda>c. c = srcCTE) slot s \<rbrace>
   setUntypedCapAsFull (cteCap srcCTE) cap slot
   \<lbrace>\<lambda>rv s. valid_mdb' s\<rbrace>" apply (clarsimp simp:valid_mdb'_def) apply (wp setUntypedCapAsFull_ctes) apply (subgoal_tac "mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot
              (cteCap_update (\<lambda>_.  maskedAsFull (cteCap srcCTE) cap)))") apply (frule mdb_inv_preserve.untyped_inc') apply (clarsimp simp:modify_map_def max_free_index_def
        maskedAsFull_def isCap_simps cte_wp_at_ctes_of
        split:if_splits) apply (clarsimp simp:valid_mdb_ctes_def mdb_inv_preserve.preserve_stuff)+ apply (clarsimp simp:mdb_inv_preserve.by_products[OF mdb_inv_preserve_sym]) apply (clarsimp simp:maskedAsFull_def cte_wp_at_ctes_of split:if_splits) apply (erule(1) mdb_inv_preserve_updateCap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' (\<lambda>c. c = srcCTE) slot s\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap slot \<lbrace>\<lambda>rv. valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) slot s\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap slot \<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> cte_wp_at' (\<lambda>c. c = srcCTE) slot s \<Longrightarrow> cte_wp_at' (\<lambda>c. c = srcCTE) slot s \<and> valid_mdb_ctes (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) slot s; mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. c = srcCTE) slot s \<and> valid_mdb_ctes (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))
 2. \<And>s. valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) slot s \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))) proof (prove)
goal (4 subgoals):
 1. \<And>s x cte cte'. \<lbrakk>valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) slot s; mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))); ctes_of s x = Some cte; modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)) x = Some cte'; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte') \<subseteq> usableUntypedRange (cteCap cte)
 2. \<And>s. \<lbrakk>valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) slot s; mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))\<rbrakk> \<Longrightarrow> untyped_inc' (ctes_of s)
 3. \<And>s. \<lbrakk>valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) slot s; mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))); untyped_inc' (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. c = srcCTE) slot s \<and> valid_mdb_ctes (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))
 4. \<And>s. valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) slot s \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) slot s; mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))\<rbrakk> \<Longrightarrow> untyped_inc' (ctes_of s)
 2. \<And>s. \<lbrakk>valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) slot s; mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))); untyped_inc' (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. c = srcCTE) slot s \<and> valid_mdb_ctes (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))
 3. \<And>s. valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) slot s \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))); untyped_inc' (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))); valid_dlist (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))); caps_contained' (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))); mdb_chunked (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))); untyped_mdb' (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))); class_links (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))); distinct_zombies (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))); irq_control (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))); reply_masters_rvk_fb (ctes_of s); cte_wp_at' (\<lambda>c. c = srcCTE) slot s\<rbrakk> \<Longrightarrow> mdb_chain_0 (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))) \<and> valid_nullcaps (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))) \<and> reply_masters_rvk_fb (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))
 2. \<And>s. valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) slot s \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) slot s \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s slot = Some srcCTE; isUntypedCap (cteCap srcCTE); isUntypedCap cap; capPtr (cteCap srcCTE) = capPtr cap; capBlockSize (cteCap srcCTE) = capBlockSize cap\<rbrakk> \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE)))) proof (prove)
goal:
No subgoals!