theory Finalise_AC

lemma reply_cap_descends_from_master0:
  "\<lbrakk> invs s; tcb_at t s \<rbrakk>
     \<Longrightarrow> \<forall>sl\<in>descendants_of (t, tcb_cnode_index 2) (cdt s).
           \<exists>R. caps_of_state s sl = Some (ReplyCap t False R)" apply (subgoal_tac "cte_wp_at (\<lambda>c. (is_master_reply_cap c \<and> obj_ref_of c = t) \<or> c = NullCap)
                                (t, tcb_cnode_index 2) s") apply (clarsimp simp: invs_def valid_state_def valid_mdb_def2 is_cap_simps
                         valid_reply_caps_def cte_wp_at_caps_of_state) apply (erule disjE) apply (unfold reply_mdb_def reply_masters_mdb_def)[1] apply (elim conjE) apply (erule_tac x="(t, tcb_cnode_index 2)" in allE) apply (erule_tac x=t in allE)+ apply (fastforce simp: unique_reply_caps_def is_cap_simps) apply (fastforce dest: mdb_cte_at_Null_descendants) apply (clarsimp simp: tcb_cap_wp_at invs_valid_objs
                        tcb_cap_cases_def is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; tcb_at t s\<rbrakk> \<Longrightarrow> \<forall>sl\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). \<exists>R. caps_of_state s sl = Some (ReplyCap t False R) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; tcb_at t s; cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t \<or> c = NullCap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<forall>sl\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). \<exists>R. caps_of_state s sl = Some (ReplyCap t False R)
 2. \<lbrakk>invs s; tcb_at t s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t \<or> c = NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (2 subgoals):
 1. \<And>a b cap. \<lbrakk>tcb_at t s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); valid_pspace s; caps_of_state s (t, tcb_cnode_index 2) = Some cap; (\<exists>x R. cap = ReplyCap x True R) \<and> obj_ref_of cap = t \<or> cap = NullCap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (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); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s\<rbrakk> \<Longrightarrow> \<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)
 2. \<lbrakk>invs s; tcb_at t s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t \<or> c = NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (3 subgoals):
 1. \<And>a b cap. \<lbrakk>tcb_at t s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); valid_pspace s; caps_of_state s (t, tcb_cnode_index 2) = Some cap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (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); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; (\<exists>x R. cap = ReplyCap x True R) \<and> obj_ref_of cap = t\<rbrakk> \<Longrightarrow> \<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)
 2. \<And>a b cap. \<lbrakk>tcb_at t s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); valid_pspace s; caps_of_state s (t, tcb_cnode_index 2) = Some cap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (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); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cap = NullCap\<rbrakk> \<Longrightarrow> \<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)
 3. \<lbrakk>invs s; tcb_at t s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t \<or> c = NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (3 subgoals):
 1. \<And>a b cap. \<lbrakk>tcb_at t s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); valid_pspace s; caps_of_state s (t, tcb_cnode_index 2) = Some cap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (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_caps_mdb (cdt s) (caps_of_state s) \<and> (\<forall>ptr t rights. caps_of_state s ptr = Some (ReplyCap t True rights) \<longrightarrow> cdt s ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights'))); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; (\<exists>x R. cap = ReplyCap x True R) \<and> obj_ref_of cap = t\<rbrakk> \<Longrightarrow> \<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)
 2. \<And>a b cap. \<lbrakk>tcb_at t s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); valid_pspace s; caps_of_state s (t, tcb_cnode_index 2) = Some cap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (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); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cap = NullCap\<rbrakk> \<Longrightarrow> \<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)
 3. \<lbrakk>invs s; tcb_at t s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t \<or> c = NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (3 subgoals):
 1. \<And>a b cap. \<lbrakk>tcb_at t s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); valid_pspace s; caps_of_state s (t, tcb_cnode_index 2) = Some cap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (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); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; reply_caps_mdb (cdt s) (caps_of_state s); \<forall>ptr t rights. caps_of_state s ptr = Some (ReplyCap t True rights) \<longrightarrow> cdt s ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); \<exists>x R. cap = ReplyCap x True R; obj_ref_of cap = t\<rbrakk> \<Longrightarrow> \<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)
 2. \<And>a b cap. \<lbrakk>tcb_at t s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); valid_pspace s; caps_of_state s (t, tcb_cnode_index 2) = Some cap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (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); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cap = NullCap\<rbrakk> \<Longrightarrow> \<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)
 3. \<lbrakk>invs s; tcb_at t s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t \<or> c = NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (3 subgoals):
 1. \<And>a b cap. \<lbrakk>tcb_at t s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); valid_pspace s; caps_of_state s (t, tcb_cnode_index 2) = Some cap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (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); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; reply_caps_mdb (cdt s) (caps_of_state s); \<exists>x R. cap = ReplyCap x True R; obj_ref_of cap = t; \<forall>ta rights. caps_of_state s (t, tcb_cnode_index 2) = Some (ReplyCap ta True rights) \<longrightarrow> cdt s (t, tcb_cnode_index 2) = None \<and> (\<forall>ptr'\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap ta False rights'))\<rbrakk> \<Longrightarrow> \<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)
 2. \<And>a b cap. \<lbrakk>tcb_at t s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); valid_pspace s; caps_of_state s (t, tcb_cnode_index 2) = Some cap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (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); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cap = NullCap\<rbrakk> \<Longrightarrow> \<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)
 3. \<lbrakk>invs s; tcb_at t s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t \<or> c = NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (3 subgoals):
 1. \<And>a b cap. \<lbrakk>tcb_at t s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); valid_pspace s; caps_of_state s (t, tcb_cnode_index 2) = Some cap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (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); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; reply_caps_mdb (cdt s) (caps_of_state s); \<exists>x R. cap = ReplyCap x True R; obj_ref_of cap = t; has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; \<forall>rights. caps_of_state s (t, tcb_cnode_index 2) = Some (ReplyCap t True rights) \<longrightarrow> cdt s (t, tcb_cnode_index 2) = None \<and> (\<forall>ptr'\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<Longrightarrow> \<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)
 2. \<And>a b cap. \<lbrakk>tcb_at t s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); valid_pspace s; caps_of_state s (t, tcb_cnode_index 2) = Some cap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (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); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cap = NullCap\<rbrakk> \<Longrightarrow> \<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)
 3. \<lbrakk>invs s; tcb_at t s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t \<or> c = NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (2 subgoals):
 1. \<And>a b cap. \<lbrakk>tcb_at t s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); valid_pspace s; caps_of_state s (t, tcb_cnode_index 2) = Some cap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (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); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cap = NullCap\<rbrakk> \<Longrightarrow> \<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)
 2. \<lbrakk>invs s; tcb_at t s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t \<or> c = NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; tcb_at t s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t \<or> c = NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal:
No subgoals!