theory CSpace_AI

lemma set_untyped_cap_as_full_valid_mdb:
  "\<lbrace>valid_mdb and cte_wp_at ((=) src_cap) src\<rbrace>
   set_untyped_cap_as_full src_cap c src
   \<lbrace>\<lambda>rv. valid_mdb\<rbrace>" apply (simp add:valid_mdb_def set_untyped_cap_as_full_def split del: if_split) apply (wp set_cap_mdb_cte_at) apply (wps set_cap_rvk_cdt_ct_ms) apply wpsimp+ apply (intro conjI impI) apply (clarsimp simp:is_cap_simps free_index_update_def split:cap.splits)+ apply (simp_all add:cte_wp_at_caps_of_state) unfolding fun_upd_def[symmetric] apply (simp_all add: untyped_mdb_update_free_index reply_mdb_update_free_index
                             untyped_inc_update_free_index valid_arch_mdb_updates) apply (erule descendants_inc_minor) apply (clarsimp simp:cte_wp_at_caps_of_state swp_def) apply (clarsimp simp: free_index_update_def cap_range_def split:cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb and cte_wp_at ((=) src_cap) src\<rbrace> set_untyped_cap_as_full src_cap c src \<lbrace>\<lambda>rv. valid_mdb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) and cte_wp_at ((=) src_cap) src\<rbrace> if is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c then set_cap (max_free_index_update src_cap) src else return () \<lbrace>\<lambda>rv s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c \<Longrightarrow> \<lbrace>?P'2\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace>
 2. \<not> (is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c) \<Longrightarrow> \<lbrace>?R1\<rbrace> return () \<lbrace>\<lambda>rv s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace>
 3. \<And>s. ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) and cte_wp_at ((=) src_cap) src) s \<Longrightarrow> (is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c \<longrightarrow> (mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<and> (src \<in> dom (cdt s) \<union> ran (cdt s) \<longrightarrow> NullCap \<noteq> max_free_index_update src_cap)) \<and> ?P'2 s) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c) \<longrightarrow> ?R1 s) proof (prove)
goal (3 subgoals):
 1. \<And>prev_s. is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c \<Longrightarrow> \<lbrace>?P4 prev_s\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s'. untyped_mdb (cdt prev_s) ((caps_of_state prev_s)(src \<mapsto> max_free_index_update src_cap)) \<and> descendants_inc (cdt prev_s) ((caps_of_state prev_s)(src \<mapsto> max_free_index_update src_cap)) \<and> no_mloop (cdt prev_s) \<and> untyped_inc (cdt prev_s) ((caps_of_state prev_s)(src \<mapsto> max_free_index_update src_cap)) \<and> ut_revocable (is_original_cap prev_s) ((caps_of_state prev_s)(src \<mapsto> max_free_index_update src_cap)) \<and> irq_revocable (is_original_cap prev_s) ((caps_of_state prev_s)(src \<mapsto> max_free_index_update src_cap)) \<and> reply_master_revocable (is_original_cap prev_s) ((caps_of_state prev_s)(src \<mapsto> max_free_index_update src_cap)) \<and> reply_mdb (cdt prev_s) ((caps_of_state prev_s)(src \<mapsto> max_free_index_update src_cap)) \<and> valid_arch_mdb (is_original_cap prev_s) ((caps_of_state prev_s)(src \<mapsto> max_free_index_update src_cap))\<rbrace>
 2. \<not> (is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c) \<Longrightarrow> \<lbrace>?R1\<rbrace> return () \<lbrace>\<lambda>rv s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace>
 3. \<And>s. ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) and cte_wp_at ((=) src_cap) src) s \<Longrightarrow> (is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c \<longrightarrow> (mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<and> (src \<in> dom (cdt s) \<union> ran (cdt s) \<longrightarrow> NullCap \<noteq> max_free_index_update src_cap)) \<and> ?P4 s s) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c) \<longrightarrow> ?R1 s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> (src \<in> dom (cdt s) \<longrightarrow> NullCap \<noteq> max_free_index_update src_cap) \<and> (src \<in> ran (cdt s) \<longrightarrow> NullCap \<noteq> max_free_index_update src_cap) \<and> untyped_mdb (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a) \<and> descendants_inc (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a) \<and> untyped_inc (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a) \<and> ut_revocable (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a) \<and> irq_revocable (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a) \<and> reply_master_revocable (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a) \<and> reply_mdb (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a) \<and> valid_arch_mdb (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a) proof (prove)
goal (10 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; src \<in> dom (cdt s)\<rbrakk> \<Longrightarrow> NullCap \<noteq> max_free_index_update src_cap
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; src \<in> ran (cdt s)\<rbrakk> \<Longrightarrow> NullCap \<noteq> max_free_index_update src_cap
 3. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> untyped_mdb (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 4. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> descendants_inc (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 5. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> untyped_inc (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 6. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> ut_revocable (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 7. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 8. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 9. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> reply_mdb (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 10. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a) proof (prove)
goal (8 subgoals):
 1. \<And>s dev deva ra bitsa f fa. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) (UntypedCap dev ra bitsa f)) src s; src_cap = UntypedCap dev ra bitsa f; c = UntypedCap deva ra bitsa fa\<rbrakk> \<Longrightarrow> untyped_mdb (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update (UntypedCap dev ra bitsa f)) else caps_of_state s a)
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> descendants_inc (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 3. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> untyped_inc (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 4. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> ut_revocable (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 5. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 6. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 7. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> reply_mdb (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 8. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at ((=) src_cap) src s; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a) proof (prove)
goal (8 subgoals):
 1. \<And>s dev deva ra bitsa f fa. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some (UntypedCap dev ra bitsa f); src_cap = UntypedCap dev ra bitsa f; c = UntypedCap deva ra bitsa fa\<rbrakk> \<Longrightarrow> untyped_mdb (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update (UntypedCap dev ra bitsa f)) else caps_of_state s a)
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> descendants_inc (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 3. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> untyped_inc (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 4. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> ut_revocable (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 5. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 6. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 7. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> reply_mdb (cdt s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a)
 8. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap s) (\<lambda>a. if a = src then Some (max_free_index_update src_cap) else caps_of_state s a) proof (prove)
goal (8 subgoals):
 1. \<And>s dev deva ra bitsa f fa. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some (UntypedCap dev ra bitsa f); src_cap = UntypedCap dev ra bitsa f; c = UntypedCap deva ra bitsa fa\<rbrakk> \<Longrightarrow> untyped_mdb (cdt s) ((caps_of_state s)(src \<mapsto> max_free_index_update (UntypedCap dev ra bitsa f)))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> descendants_inc (cdt s) ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap))
 3. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> untyped_inc (cdt s) ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap))
 4. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> ut_revocable (is_original_cap s) ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap))
 5. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap s) ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap))
 6. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap s) ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap))
 7. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> reply_mdb (cdt s) ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap))
 8. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap s) ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> descendants_inc (cdt s) ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s)
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (caps_of_state s). cap_class (the (((caps_of_state s)(src \<mapsto> max_free_index_update src_cap)) x)) = cap_class (the (caps_of_state s x)) \<and> cap_range (the (((caps_of_state s)(src \<mapsto> max_free_index_update src_cap)) x)) = cap_range (the (caps_of_state s x)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some src_cap; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (caps_of_state s). cap_class (the (((caps_of_state s)(src \<mapsto> max_free_index_update src_cap)) x)) = cap_class (the (caps_of_state s x)) \<and> cap_range (the (((caps_of_state s)(src \<mapsto> max_free_index_update src_cap)) x)) = cap_range (the (caps_of_state s x)) proof (prove)
goal:
No subgoals!