theory CSpace_AI

lemma cap_insert_valid_pspace:
  "\<lbrace>valid_pspace and cte_wp_at ((=) cap.NullCap) dest
                 and valid_cap cap and tcb_cap_valid cap dest
      and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>p'. dest \<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 cap))\<rbrace>
     cap_insert cap src dest
   \<lbrace>\<lambda>_. valid_pspace\<rbrace>" unfolding cap_insert_def apply (simp add: update_cdt_def) apply (wp new_cap_valid_pspace set_cdt_valid_pspace set_cdt_cte_at
    set_untyped_cap_as_full_cte_wp_at set_untyped_cap_as_full_valid_cap
    set_cdt_valid_cap hoare_drop_imps set_untyped_cap_as_full_tcb_cap_valid
    set_untyped_cap_as_full_valid_pspace | simp split del: if_split)+ apply (wp hoare_vcg_ball_lift hoare_vcg_all_lift hoare_vcg_imp_lift) apply clarsimp apply (wp hoare_vcg_disj_lift set_untyped_cap_as_full_cte_wp_at_neg
                 set_untyped_cap_as_full_cte_wp_at get_cap_wp)+ apply (intro allI impI conjI) apply (clarsimp simp: cte_wp_at_caps_of_state)+ apply (rule ccontr) apply clarsimp apply (drule bspec) apply simp apply (drule_tac x = xa in spec,drule_tac x = xb in spec) apply (subgoal_tac "(xa,xb) = src") apply (clarsimp simp: masked_as_full_def if_distrib split:if_splits) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace and cte_wp_at ((=) NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>p'. dest \<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 cap)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace and cte_wp_at ((=) NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>p'. dest \<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 cap)\<rbrace> do src_cap <- get_cap src;
dest_original <- return $ is_cap_revocable cap src_cap;
old_cap <- get_cap dest;
assert (old_cap = NullCap);
set_untyped_cap_as_full src_cap cap src;
set_cap cap dest;
is_original <- gets is_original_cap;
src_parent <- return $ should_be_parent_of src_cap (is_original src) cap dest_original;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
update_cdt (\<lambda>cdt. cdt(dest := if src_parent then Some src else cdt src));
do_extended_op (cap_insert_ext src_parent src dest src_p dest_p);
set_original dest dest_original
od \<lbrace>\<lambda>_. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace and cte_wp_at ((=) NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap cap src;
y <- set_cap cap dest;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
y <- do t <- gets cdt;
set_cdt (t(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else t src))
od;
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap)) src dest src_p dest_p);
set_original dest (is_cap_revocable cap src_cap)
od \<lbrace>\<lambda>_. valid_pspace\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>src_cap x. \<lbrace>?P'54 src_cap x ()\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap\<rbrace>
 2. \<And>src_cap x. \<lbrace>?B8 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>\<lambda>y s. ((dest \<noteq> src \<and> cte_wp_at ((=) NullCap) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. NullCap = masked_as_full a cap) src s) \<and> cte_wp_at ((=) src_cap) src s) \<and> s \<turnstile> cap \<and> tcb_cap_valid cap dest s \<and> (valid_pspace and cte_wp_at ((=) src_cap) src) s \<and> ?P'54 src_cap x y s\<rbrace>
 3. \<And>src_cap. \<lbrace>?B7 src_cap\<rbrace> get_cap dest \<lbrace>?B8 src_cap\<rbrace>
 4. \<lbrace>?Q6\<rbrace> get_cap src \<lbrace>?B7\<rbrace>
 5. \<And>s. (valid_pspace and cte_wp_at ((=) NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>src_cap x r a b. r \<in> obj_refs cap \<Longrightarrow> \<lbrace>?P'77 src_cap x () r a b\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. \<not> (dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s)\<rbrace>
 2. \<And>src_cap x r a b. r \<in> obj_refs cap \<Longrightarrow> \<lbrace>?Q'76 src_cap x () r a b\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap\<rbrace>
 3. \<And>src_cap x. \<lbrace>?B8 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>\<lambda>y s. ((dest \<noteq> src \<and> cte_wp_at ((=) NullCap) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. NullCap = masked_as_full a cap) src s) \<and> cte_wp_at ((=) src_cap) src s) \<and> s \<turnstile> cap \<and> tcb_cap_valid cap dest s \<and> (valid_pspace and cte_wp_at ((=) src_cap) src) s \<and> (\<forall>xa\<in>obj_refs cap. \<forall>xb xc. ?P'77 src_cap x y xa xb xc s \<or> ?Q'76 src_cap x y xa xb xc s)\<rbrace>
 4. \<And>src_cap. \<lbrace>?B7 src_cap\<rbrace> get_cap dest \<lbrace>?B8 src_cap\<rbrace>
 5. \<lbrace>?Q6\<rbrace> get_cap src \<lbrace>?B7\<rbrace>
 6. \<And>s. (valid_pspace and cte_wp_at ((=) NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>src_cap x r a b. r \<in> obj_refs cap \<Longrightarrow> \<lbrace>?P'77 src_cap x () r a b\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. dest = (a, b) \<or> \<not> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s\<rbrace>
 2. \<And>src_cap x r a b. r \<in> obj_refs cap \<Longrightarrow> \<lbrace>?Q'76 src_cap x () r a b\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap\<rbrace>
 3. \<And>src_cap x. \<lbrace>?B8 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>\<lambda>y s. ((dest \<noteq> src \<and> cte_wp_at ((=) NullCap) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. NullCap = masked_as_full a cap) src s) \<and> cte_wp_at ((=) src_cap) src s) \<and> s \<turnstile> cap \<and> tcb_cap_valid cap dest s \<and> (valid_pspace and cte_wp_at ((=) src_cap) src) s \<and> (\<forall>xa\<in>obj_refs cap. \<forall>xb xc. ?P'77 src_cap x y xa xb xc s \<or> ?Q'76 src_cap x y xa xb xc s)\<rbrace>
 4. \<And>src_cap. \<lbrace>?B7 src_cap\<rbrace> get_cap dest \<lbrace>?B8 src_cap\<rbrace>
 5. \<lbrace>?Q6\<rbrace> get_cap src \<lbrace>?B7\<rbrace>
 6. \<And>s. (valid_pspace and cte_wp_at ((=) NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_pspace and cte_wp_at ((=) NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> (\<forall>capb. cte_wp_at ((=) capb) dest s \<longrightarrow> capb = NullCap \<longrightarrow> ((dest \<noteq> src \<and> cte_wp_at ((=) NullCap) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. NullCap = masked_as_full a cap) src s) \<and> cte_wp_at ((=) capa) src s) \<and> s \<turnstile> cap \<and> tcb_cap_valid cap dest s \<and> (valid_pspace and cte_wp_at ((=) capa) src) s \<and> (\<forall>x\<in>obj_refs cap. \<forall>xa xb. (dest = (xa, xb) \<or> ((xa, xb) \<noteq> src \<and> \<not> cte_wp_at (\<lambda>a. x \<in> obj_refs a) (xa, xb) s \<or> (xa, xb) = src \<and> \<not> cte_wp_at (\<lambda>a. x \<in> obj_refs (masked_as_full a cap)) src s) \<and> cte_wp_at ((=) capa) src s) \<or> (((xa, xb) \<noteq> src \<and> cte_wp_at (Not \<circ> is_zombie) (xa, xb) s \<or> (xa, xb) = src \<and> cte_wp_at (\<lambda>a. (Not \<circ> is_zombie) (masked_as_full a cap)) src s) \<and> cte_wp_at ((=) capa) src s) \<and> \<not> is_zombie cap)) proof (prove)
goal (6 subgoals):
 1. \<And>s capa capaa. \<lbrakk>(valid_pspace and cte_wp_at ((=) NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap\<rbrakk> \<Longrightarrow> dest \<noteq> src \<and> cte_wp_at ((=) NullCap) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. NullCap = masked_as_full a cap) src s
 2. \<And>s capa capaa. \<lbrakk>(valid_pspace and cte_wp_at ((=) NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap\<rbrakk> \<Longrightarrow> cte_wp_at ((=) capa) src s
 3. \<And>s capa capaa. \<lbrakk>(valid_pspace and cte_wp_at ((=) NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 4. \<And>s capa capaa. \<lbrakk>(valid_pspace and cte_wp_at ((=) NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap\<rbrakk> \<Longrightarrow> tcb_cap_valid cap dest s
 5. \<And>s capa capaa. \<lbrakk>(valid_pspace and cte_wp_at ((=) NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap\<rbrakk> \<Longrightarrow> (valid_pspace and cte_wp_at ((=) capa) src) s
 6. \<And>s capa capaa. \<lbrakk>(valid_pspace and cte_wp_at ((=) NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap\<rbrakk> \<Longrightarrow> \<forall>x\<in>obj_refs cap. \<forall>xa xb. (dest = (xa, xb) \<or> ((xa, xb) \<noteq> src \<and> \<not> cte_wp_at (\<lambda>a. x \<in> obj_refs a) (xa, xb) s \<or> (xa, xb) = src \<and> \<not> cte_wp_at (\<lambda>a. x \<in> obj_refs (masked_as_full a cap)) src s) \<and> cte_wp_at ((=) capa) src s) \<or> (((xa, xb) \<noteq> src \<and> cte_wp_at (Not \<circ> is_zombie) (xa, xb) s \<or> (xa, xb) = src \<and> cte_wp_at (\<lambda>a. (Not \<circ> is_zombie) (masked_as_full a cap)) src s) \<and> cte_wp_at ((=) capa) src s) \<and> \<not> is_zombie cap proof (prove)
goal (1 subgoal):
 1. \<And>s capa x xa xb. \<lbrakk>caps_of_state s src = Some capa; x \<in> obj_refs cap; valid_pspace s; caps_of_state s dest = Some NullCap; s \<turnstile> cap; tcb_cap_valid cap dest s; \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, 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 cap; dest \<noteq> (xa, xb); (xa, xb) = src \<or> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> x \<in> obj_refs cap); ((xa, xb) = src \<or> (\<forall>cap. caps_of_state s (xa, xb) = Some cap \<longrightarrow> is_zombie cap)) \<and> ((xa, xb) = src \<longrightarrow> is_zombie capa) \<or> is_zombie cap\<rbrakk> \<Longrightarrow> (xa, xb) = src \<and> x \<notin> obj_refs capa proof (prove)
goal (1 subgoal):
 1. \<And>s capa x xa xb. \<lbrakk>caps_of_state s src = Some capa; x \<in> obj_refs cap; valid_pspace s; caps_of_state s dest = Some NullCap; s \<turnstile> cap; tcb_cap_valid cap dest s; \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, 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 cap; dest \<noteq> (xa, xb); (xa, xb) = src \<or> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> x \<in> obj_refs cap); ((xa, xb) = src \<or> (\<forall>cap. caps_of_state s (xa, xb) = Some cap \<longrightarrow> is_zombie cap)) \<and> ((xa, xb) = src \<longrightarrow> is_zombie capa) \<or> is_zombie cap; \<not> ((xa, xb) = src \<and> x \<notin> obj_refs capa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s capa x xa xb. \<lbrakk>caps_of_state s src = Some capa; x \<in> obj_refs cap; valid_pspace s; caps_of_state s dest = Some NullCap; s \<turnstile> cap; tcb_cap_valid cap dest s; \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, 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 cap; dest \<noteq> (xa, xb); (xa, xb) = src \<or> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> x \<in> obj_refs cap); ((xa, xb) = src \<or> (\<forall>cap. caps_of_state s (xa, xb) = Some cap \<longrightarrow> is_zombie cap)) \<and> ((xa, xb) = src \<longrightarrow> is_zombie capa) \<or> is_zombie cap; (xa, xb) = src \<longrightarrow> x \<in> obj_refs capa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s capa x xa xb. \<lbrakk>caps_of_state s src = Some capa; x \<in> obj_refs cap; valid_pspace s; caps_of_state s dest = Some NullCap; s \<turnstile> cap; tcb_cap_valid cap dest s; dest \<noteq> (xa, xb); (xa, xb) = src \<or> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> x \<in> obj_refs cap); ((xa, xb) = src \<or> (\<forall>cap. caps_of_state s (xa, xb) = Some cap \<longrightarrow> is_zombie cap)) \<and> ((xa, xb) = src \<longrightarrow> is_zombie capa) \<or> is_zombie cap; (xa, xb) = src \<longrightarrow> x \<in> obj_refs capa\<rbrakk> \<Longrightarrow> ?r139 s capa x xa xb \<in> obj_refs cap
 2. \<And>s capa x xa xb. \<lbrakk>caps_of_state s src = Some capa; x \<in> obj_refs cap; valid_pspace s; caps_of_state s dest = Some NullCap; s \<turnstile> cap; tcb_cap_valid cap dest s; dest \<noteq> (xa, xb); (xa, xb) = src \<or> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> x \<in> obj_refs cap); ((xa, xb) = src \<or> (\<forall>cap. caps_of_state s (xa, xb) = Some cap \<longrightarrow> is_zombie cap)) \<and> ((xa, xb) = src \<longrightarrow> is_zombie capa) \<or> is_zombie cap; (xa, xb) = src \<longrightarrow> x \<in> obj_refs capa; \<forall>a b. dest \<noteq> (a, b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> ?r139 s capa x xa xb \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s capa x xa xb. \<lbrakk>caps_of_state s src = Some capa; x \<in> obj_refs cap; valid_pspace s; caps_of_state s dest = Some NullCap; s \<turnstile> cap; tcb_cap_valid cap dest s; dest \<noteq> (xa, xb); (xa, xb) = src \<or> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> x \<in> obj_refs cap); ((xa, xb) = src \<or> (\<forall>cap. caps_of_state s (xa, xb) = Some cap \<longrightarrow> is_zombie cap)) \<and> ((xa, xb) = src \<longrightarrow> is_zombie capa) \<or> is_zombie cap; (xa, xb) = src \<longrightarrow> x \<in> obj_refs capa; \<forall>a b. dest \<noteq> (a, b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> x \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s capa x xa xb. \<lbrakk>caps_of_state s src = Some capa; x \<in> obj_refs cap; valid_pspace s; caps_of_state s dest = Some NullCap; s \<turnstile> cap; tcb_cap_valid cap dest s; dest \<noteq> (xa, xb); (xa, xb) = src \<or> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> x \<in> obj_refs cap); ((xa, xb) = src \<or> (\<forall>cap. caps_of_state s (xa, xb) = Some cap \<longrightarrow> is_zombie cap)) \<and> ((xa, xb) = src \<longrightarrow> is_zombie capa) \<or> is_zombie cap; (xa, xb) = src \<longrightarrow> x \<in> obj_refs capa; dest \<noteq> (xa, xb) \<and> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> x \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s capa x xa xb. \<lbrakk>caps_of_state s src = Some capa; x \<in> obj_refs cap; valid_pspace s; caps_of_state s dest = Some NullCap; s \<turnstile> cap; tcb_cap_valid cap dest s; dest \<noteq> (xa, xb); (xa, xb) = src \<or> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> x \<in> obj_refs cap); ((xa, xb) = src \<or> (\<forall>cap. caps_of_state s (xa, xb) = Some cap \<longrightarrow> is_zombie cap)) \<and> ((xa, xb) = src \<longrightarrow> is_zombie capa) \<or> is_zombie cap; (xa, xb) = src \<longrightarrow> x \<in> obj_refs capa; dest \<noteq> (xa, xb) \<and> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> x \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; (xa, xb) = src\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa x xa xb. \<lbrakk>caps_of_state s src = Some capa; x \<in> obj_refs cap; valid_pspace s; caps_of_state s dest = Some NullCap; s \<turnstile> cap; tcb_cap_valid cap dest s; dest \<noteq> (xa, xb); (xa, xb) = src \<or> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> x \<in> obj_refs cap); ((xa, xb) = src \<or> (\<forall>cap. caps_of_state s (xa, xb) = Some cap \<longrightarrow> is_zombie cap)) \<and> ((xa, xb) = src \<longrightarrow> is_zombie capa) \<or> is_zombie cap; (xa, xb) = src \<longrightarrow> x \<in> obj_refs capa; dest \<noteq> (xa, xb) \<and> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> x \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap\<rbrakk> \<Longrightarrow> (xa, xb) = src proof (prove)
goal (1 subgoal):
 1. \<And>s capa x xa xb. \<lbrakk>caps_of_state s src = Some capa; x \<in> obj_refs cap; valid_pspace s; caps_of_state s dest = Some NullCap; s \<turnstile> cap; tcb_cap_valid cap dest s; dest \<noteq> (xa, xb); (xa, xb) = src \<or> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> x \<in> obj_refs cap); ((xa, xb) = src \<or> (\<forall>cap. caps_of_state s (xa, xb) = Some cap \<longrightarrow> is_zombie cap)) \<and> ((xa, xb) = src \<longrightarrow> is_zombie capa) \<or> is_zombie cap; (xa, xb) = src \<longrightarrow> x \<in> obj_refs capa; dest \<noteq> (xa, xb) \<and> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> x \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (xa, xb) = Some cap \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap\<rbrakk> \<Longrightarrow> (xa, xb) = src proof (prove)
goal:
No subgoals!