theory IpcCancel_AI

lemma reply_cap_unique_descendant:
  "\<lbrakk> invs s; tcb_at t s \<rbrakk> \<Longrightarrow>
   \<forall>sl\<in>descendants_of (t, tcb_cnode_index 2) (cdt s).  \<forall>sl'. sl' \<noteq> sl \<longrightarrow>
      sl' \<notin> descendants_of (t, tcb_cnode_index 2) (cdt s)" apply (subgoal_tac "cte_wp_at (\<lambda>c. (is_master_reply_cap c \<and> obj_ref_of c = t)
                                     \<or> c = cap.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 (fastforce simp: reply_mdb_def is_cap_simps dest: unique_reply_capsD) 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). \<forall>sl'. sl' \<noteq> sl \<longrightarrow> sl' \<notin> descendants_of (t, tcb_cnode_index 2) (cdt s) 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). \<forall>sl'. sl' \<noteq> sl \<longrightarrow> sl' \<notin> descendants_of (t, tcb_cnode_index 2) (cdt s)
 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 aa ba. \<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; aa = a \<longrightarrow> ba \<noteq> b; (aa, ba) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s)\<rbrakk> \<Longrightarrow> False
 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 aa ba. \<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; aa = a \<longrightarrow> ba \<noteq> b; (aa, ba) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); (\<exists>x R. cap = ReplyCap x True R) \<and> obj_ref_of cap = t\<rbrakk> \<Longrightarrow> False
 2. \<And>a b cap aa ba. \<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; aa = a \<longrightarrow> ba \<noteq> b; (aa, ba) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); cap = NullCap\<rbrakk> \<Longrightarrow> False
 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 aa ba. \<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; aa = a \<longrightarrow> ba \<noteq> b; (aa, ba) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); cap = NullCap\<rbrakk> \<Longrightarrow> False
 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!