theory ArchTcb_AI

lemma checked_insert_tcb_invs[wp]: (* arch specific *)
  "\<lbrace>invs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref)
        and K (is_cnode_or_valid_arch new_cap) and valid_cap new_cap
        and tcb_cap_valid new_cap (target, ref)
        and K (is_pt_cap new_cap \<or> is_pd_cap new_cap
                         \<longrightarrow> cap_asid new_cap \<noteq> None)
        and (cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap
                              \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and>
                                 pt_pd_asid c = pt_pd_asid new_cap) src_slot)\<rbrace>
     check_cap_at new_cap src_slot
      (check_cap_at (cap.ThreadCap target) slot
       (cap_insert new_cap src_slot (target, ref))) \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: check_cap_at_def) apply (rule hoare_pre) apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (frule caps_of_state_valid_cap[where p=src_slot], fastforce) apply (frule caps_of_state_valid_cap[where p=slot], fastforce) apply (rule conjI, simp only: ex_cte_cap_wp_to_def) apply (rule_tac x=slot in exI) apply (clarsimp simp: cte_wp_at_caps_of_state same_object_as_cte_refs) apply (clarsimp simp: same_object_as_def2 cap_master_cap_simps
                  dest!: cap_master_cap_eqDs) apply (clarsimp simp: valid_cap_def[where c="cap.ThreadCap x" for x]) apply (erule cte_wp_atE[OF caps_of_state_cteD]) apply (fastforce simp: obj_at_def is_obj_defs) apply clarsimp apply (rule conjI) apply clarsimp apply (subgoal_tac "\<not> is_zombie new_cap") apply (simp add: same_object_zombies same_object_obj_refs) apply (erule(2) zombies_final_helperE) apply fastforce apply (fastforce simp add: cte_wp_at_caps_of_state) apply assumption apply (clarsimp simp: is_cnode_or_valid_arch_def is_cap_simps
                         is_valid_vtable_root_def) apply (rule conjI) apply (erule(1) checked_insert_is_derived, simp+) apply (auto simp: is_cnode_or_valid_arch_def is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and cte_wp_at (\<lambda>c. c = NullCap) (target, ref) and K (is_cnode_or_valid_arch new_cap) and valid_cap new_cap and tcb_cap_valid new_cap (target, ref) and K (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot\<rbrace> check_cap_at new_cap src_slot (check_cap_at (ThreadCap target) slot (cap_insert new_cap src_slot (target, ref))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and cte_wp_at (\<lambda>c. c = NullCap) (target, ref) and (\<lambda>y. is_cnode_or_valid_arch new_cap) and valid_cap new_cap and tcb_cap_valid new_cap (target, ref) and (\<lambda>y. (is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y)) \<and> (is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y))) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot\<rbrace> do cap' <- get_cap src_slot;
when (same_object_as new_cap cap') (do cap' <- get_cap slot;
when (same_object_as (ThreadCap target) cap') (cap_insert new_cap src_slot (target, ref))
od)
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> do cap' <- get_cap src_slot;
when (same_object_as new_cap cap') (do cap' <- get_cap slot;
when (same_object_as (ThreadCap target) cap') (cap_insert new_cap src_slot (target, ref))
od)
od \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>s. (invs and cte_wp_at (\<lambda>c. c = NullCap) (target, ref) and (\<lambda>y. is_cnode_or_valid_arch new_cap) and valid_cap new_cap and tcb_cap_valid new_cap (target, ref) and (\<lambda>y. (is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y)) \<and> (is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y))) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s \<Longrightarrow> ?Q3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and cte_wp_at (\<lambda>c. c = NullCap) (target, ref) and (\<lambda>y. is_cnode_or_valid_arch new_cap) and valid_cap new_cap and tcb_cap_valid new_cap (target, ref) and (\<lambda>y. (is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y)) \<and> (is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y))) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) src_slot s \<longrightarrow> (if same_object_as new_cap cap then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (if same_object_as (ThreadCap target) cap then invs and cte_wp_at (\<lambda>c. c = NullCap) (target, ref) and valid_cap new_cap and tcb_cap_valid new_cap (target, ref) and ex_cte_cap_wp_to (appropriate_cte_cap new_cap) (target, ref) and (\<lambda>s. \<forall>r\<in>obj_refs new_cap. \<forall>p'. (target, ref) \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie new_cap) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) and (\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs new_cap - cap_irqs cap'. irq_issued irq s) src_slot s) and (\<lambda>s. \<forall>t R. new_cap = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) and K (\<not> is_master_reply_cap new_cap) else invs) s else invs) s proof (prove)
goal (1 subgoal):
 1. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap new_cap) (target, ref) s \<and> (\<forall>r\<in>obj_refs new_cap. \<forall>a b. (target = a \<longrightarrow> ref \<noteq> b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie new_cap) \<and> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (1 subgoal):
 1. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap new_cap) (target, ref) s \<and> (\<forall>r\<in>obj_refs new_cap. \<forall>a b. (target = a \<longrightarrow> ref \<noteq> b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie new_cap) \<and> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (1 subgoal):
 1. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap new_cap) (target, ref) s \<and> (\<forall>r\<in>obj_refs new_cap. \<forall>a b. (target = a \<longrightarrow> ref \<noteq> b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie new_cap) \<and> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (2 subgoals):
 1. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> \<exists>cref. cte_wp_at (\<lambda>c. appropriate_cte_cap new_cap c \<and> (target, ref) \<in> cte_refs c (interrupt_irq_node s)) cref s
 2. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> (\<forall>r\<in>obj_refs new_cap. \<forall>a b. (target = a \<longrightarrow> ref \<noteq> b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie new_cap) \<and> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (2 subgoals):
 1. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. appropriate_cte_cap new_cap c \<and> (target, ref) \<in> cte_refs c (interrupt_irq_node s)) slot s
 2. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> (\<forall>r\<in>obj_refs new_cap. \<forall>a b. (target = a \<longrightarrow> ref \<noteq> b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie new_cap) \<and> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (2 subgoals):
 1. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> appropriate_cte_cap new_cap capb \<and> ref \<in> dom tcb_cap_cases
 2. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> (\<forall>r\<in>obj_refs new_cap. \<forall>a b. (target = a \<longrightarrow> ref \<noteq> b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie new_cap) \<and> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; caps_of_state s src_slot = Some capa; caps_of_state s slot = Some (ThreadCap target); s \<turnstile> capa; s \<turnstile> ThreadCap target; cap_master_cap new_cap = cap_master_cap capa; new_cap \<noteq> NullCap; \<not> is_zombie (ThreadCap target); is_arch_cap (ThreadCap target) \<longrightarrow> (case the_arch_cap (ThreadCap target) of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True); \<not> is_untyped_cap new_cap; \<not> is_zombie new_cap; is_arch_cap new_cap \<longrightarrow> (case the_arch_cap new_cap of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True)\<rbrakk> \<Longrightarrow> \<exists>a aa b. tcb_cap_cases ref = Some (a, aa, b)
 2. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> (\<forall>r\<in>obj_refs new_cap. \<forall>a b. (target = a \<longrightarrow> ref \<noteq> b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie new_cap) \<and> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; caps_of_state s src_slot = Some capa; caps_of_state s slot = Some (ThreadCap target); s \<turnstile> capa; cap_master_cap new_cap = cap_master_cap capa; new_cap \<noteq> NullCap; \<not> is_zombie (ThreadCap target); is_arch_cap (ThreadCap target) \<longrightarrow> (case the_arch_cap (ThreadCap target) of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True); \<not> is_untyped_cap new_cap; \<not> is_zombie new_cap; is_arch_cap new_cap \<longrightarrow> (case the_arch_cap new_cap of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True); cap_aligned (ThreadCap target); tcb_at target s\<rbrakk> \<Longrightarrow> \<exists>a aa b. tcb_cap_cases ref = Some (a, aa, b)
 2. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> (\<forall>r\<in>obj_refs new_cap. \<forall>a b. (target = a \<longrightarrow> ref \<noteq> b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie new_cap) \<and> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (3 subgoals):
 1. \<And>s capa sz fun cte. \<lbrakk>invs s; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; caps_of_state s src_slot = Some capa; caps_of_state s slot = Some (ThreadCap target); s \<turnstile> capa; cap_master_cap new_cap = cap_master_cap capa; new_cap \<noteq> NullCap; \<not> is_zombie (ThreadCap target); is_arch_cap (ThreadCap target) \<longrightarrow> (case the_arch_cap (ThreadCap target) of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True); \<not> is_untyped_cap new_cap; \<not> is_zombie new_cap; is_arch_cap new_cap \<longrightarrow> (case the_arch_cap new_cap of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True); cap_aligned (ThreadCap target); tcb_at target s; kheap s (fst (target, ref)) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd (target, ref)) = Some cte; NullCap = cte\<rbrakk> \<Longrightarrow> \<exists>a aa b. tcb_cap_cases ref = Some (a, aa, b)
 2. \<And>s capa tcb getF setF restr. \<lbrakk>invs s; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; caps_of_state s src_slot = Some capa; caps_of_state s slot = Some (ThreadCap target); s \<turnstile> capa; cap_master_cap new_cap = cap_master_cap capa; new_cap \<noteq> NullCap; \<not> is_zombie (ThreadCap target); is_arch_cap (ThreadCap target) \<longrightarrow> (case the_arch_cap (ThreadCap target) of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True); \<not> is_untyped_cap new_cap; \<not> is_zombie new_cap; is_arch_cap new_cap \<longrightarrow> (case the_arch_cap new_cap of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True); cap_aligned (ThreadCap target); tcb_at target s; kheap s (fst (target, ref)) = Some (TCB tcb); tcb_cap_cases (snd (target, ref)) = Some (getF, setF, restr); NullCap = getF tcb\<rbrakk> \<Longrightarrow> \<exists>a aa b. tcb_cap_cases ref = Some (a, aa, b)
 3. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> (\<forall>r\<in>obj_refs new_cap. \<forall>a b. (target = a \<longrightarrow> ref \<noteq> b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie new_cap) \<and> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (2 subgoals):
 1. \<And>s capa tcb getF setF restr. \<lbrakk>invs s; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; caps_of_state s src_slot = Some capa; caps_of_state s slot = Some (ThreadCap target); s \<turnstile> capa; cap_master_cap new_cap = cap_master_cap capa; new_cap \<noteq> NullCap; \<not> is_zombie (ThreadCap target); is_arch_cap (ThreadCap target) \<longrightarrow> (case the_arch_cap (ThreadCap target) of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True); \<not> is_untyped_cap new_cap; \<not> is_zombie new_cap; is_arch_cap new_cap \<longrightarrow> (case the_arch_cap new_cap of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True); cap_aligned (ThreadCap target); tcb_at target s; kheap s (fst (target, ref)) = Some (TCB tcb); tcb_cap_cases (snd (target, ref)) = Some (getF, setF, restr); NullCap = getF tcb\<rbrakk> \<Longrightarrow> \<exists>a aa b. tcb_cap_cases ref = Some (a, aa, b)
 2. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> (\<forall>r\<in>obj_refs new_cap. \<forall>a b. (target = a \<longrightarrow> ref \<noteq> b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie new_cap) \<and> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (1 subgoal):
 1. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> (\<forall>r\<in>obj_refs new_cap. \<forall>a b. (target = a \<longrightarrow> ref \<noteq> b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie new_cap) \<and> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (2 subgoals):
 1. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> \<forall>r\<in>obj_refs new_cap. \<forall>a b. (target = a \<longrightarrow> ref \<noteq> b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie new_cap
 2. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (2 subgoals):
 1. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs new_cap; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap\<rbrakk> \<Longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie new_cap
 2. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (3 subgoals):
 1. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs new_cap; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; \<not> is_zombie new_cap\<rbrakk> \<Longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie new_cap
 2. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs new_cap; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap\<rbrakk> \<Longrightarrow> \<not> is_zombie new_cap
 3. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (3 subgoals):
 1. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs capa; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; \<not> is_zombie capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap
 2. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs new_cap; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap\<rbrakk> \<Longrightarrow> \<not> is_zombie new_cap
 3. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (5 subgoals):
 1. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs capa; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; \<not> is_zombie capa\<rbrakk> \<Longrightarrow> zombies_final s
 2. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs capa; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; \<not> is_zombie capa\<rbrakk> \<Longrightarrow> caps_of_state s (?p'172 s capa capb r a b cap) = Some cap
 3. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs capa; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; \<not> is_zombie capa\<rbrakk> \<Longrightarrow> r \<in> obj_refs cap
 4. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs new_cap; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap\<rbrakk> \<Longrightarrow> \<not> is_zombie new_cap
 5. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (4 subgoals):
 1. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs capa; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; \<not> is_zombie capa\<rbrakk> \<Longrightarrow> caps_of_state s (?p'172 s capa capb r a b cap) = Some cap
 2. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs capa; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; \<not> is_zombie capa\<rbrakk> \<Longrightarrow> r \<in> obj_refs cap
 3. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs new_cap; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap\<rbrakk> \<Longrightarrow> \<not> is_zombie new_cap
 4. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (3 subgoals):
 1. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs capa; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; \<not> is_zombie capa\<rbrakk> \<Longrightarrow> r \<in> obj_refs cap
 2. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs new_cap; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap\<rbrakk> \<Longrightarrow> \<not> is_zombie new_cap
 3. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (2 subgoals):
 1. \<And>s capa capb r a b cap. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb; r \<in> obj_refs new_cap; target = a \<longrightarrow> ref \<noteq> b; caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap\<rbrakk> \<Longrightarrow> \<not> is_zombie new_cap
 2. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (1 subgoal):
 1. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> is_derived (cdt s) src_slot new_cap capa \<and> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (2 subgoals):
 1. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> is_derived (cdt s) src_slot new_cap capa
 2. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal (1 subgoal):
 1. \<And>s capa capb. \<lbrakk>invs s; caps_of_state s (target, ref) = Some NullCap; is_cnode_or_valid_arch new_cap; s \<turnstile> new_cap; tcb_cap_valid new_cap (target, ref) s; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; same_object_as new_cap capa; caps_of_state s src_slot = Some capa; same_object_as (ThreadCap target) capb; caps_of_state s slot = Some capb; s \<turnstile> capa; s \<turnstile> capb\<rbrakk> \<Longrightarrow> (\<forall>irq\<in>cap_irqs new_cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>t. (\<exists>R. new_cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap new_cap proof (prove)
goal:
No subgoals!