theory Ipc_AI

lemma cap_insert_cte_wp_at:
  "\<lbrace>\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s \<and> valid_mdb s \<and> valid_objs s
    \<and> (if p = dest then P cap else cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp split:if_split_asm) apply (clarsimp simp:cap_insert_def) apply (wp set_cap_cte_wp_at | simp split del: if_split)+ apply (clarsimp simp:set_untyped_cap_as_full_def split del:if_split) apply (wp get_cap_wp)+ apply (clarsimp simp: cte_wp_at_caps_of_state) apply (clarsimp simp:cap_insert_def) apply (wp set_cap_cte_wp_at | simp split del: if_split)+ apply (clarsimp simp:set_untyped_cap_as_full_def split del:if_split) apply (wp set_cap_cte_wp_at get_cap_wp)+ apply (clarsimp simp:cte_wp_at_caps_of_state) apply (frule(1) caps_of_state_valid) apply (intro conjI impI) apply (clarsimp simp:masked_as_full_def split:if_splits)+ apply (clarsimp simp:valid_mdb_def is_derived_def) apply (drule(4) untyped_incD) apply (clarsimp simp:is_cap_simps cap_aligned_def
      dest!:valid_cap_aligned split:if_split_asm) apply (drule_tac y = "of_nat fa" in word_plus_mono_right[OF _ is_aligned_no_overflow',rotated]) apply (simp add:word_of_nat_less) apply (clarsimp simp:p_assoc_help) apply (drule(1) caps_of_state_valid)+ apply (clarsimp simp:valid_cap_def valid_untyped_def max_free_index_def) apply (clarsimp simp:masked_as_full_def split:if_splits) apply (erule impEM) apply (clarsimp simp: is_derived_def split:if_splits) apply (clarsimp simp:is_cap_simps cap_master_cap_simps) apply (clarsimp simp:is_cap_simps cap_master_cap_simps dest!:cap_master_cap_eqDs) apply (erule impEM) apply (clarsimp simp: is_derived_def split:if_splits) apply (clarsimp simp:is_cap_simps cap_master_cap_simps) apply (clarsimp simp:is_cap_simps cap_master_cap_simps dest!:cap_master_cap_eqDs) apply (clarsimp simp:is_derived_def is_cap_simps cap_master_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s \<and> valid_mdb s \<and> valid_objs s \<and> (if p = dest then P cap else cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at (is_derived (cdt s) src cap) src s \<and> valid_mdb s \<and> valid_objs s \<and> (if p = dest then P cap else cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s) \<Longrightarrow> \<lbrace>(=) s\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>p = dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; P cap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P dest\<rbrace>
 2. \<And>s. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>p = dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; P cap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<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 <- update_cdt (\<lambda>cdt. cdt(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else cdt src));
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>uu. cte_wp_at P dest\<rbrace>
 2. \<And>s. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s src_cap x. \<lbrakk>p = dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; P cap\<rbrakk> \<Longrightarrow> \<lbrace>?B29 s src_cap x ()\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>ya. cte_wp_at (\<lambda>_. True) dest\<rbrace>
 2. \<And>s src_cap x. \<lbrakk>p = dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; P cap\<rbrakk> \<Longrightarrow> \<lbrace>?B28 s src_cap x\<rbrace> assert (x = NullCap) \<lbrace>?B29 s src_cap x\<rbrace>
 3. \<And>s src_cap. \<lbrakk>p = dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; P cap\<rbrakk> \<Longrightarrow> \<lbrace>?B27 s src_cap\<rbrace> get_cap dest \<lbrace>?B28 s src_cap\<rbrace>
 4. \<And>s. \<lbrakk>p = dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; P cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 s\<rbrace> get_cap src \<lbrace>?B27 s\<rbrace>
 5. \<And>s sa. \<lbrakk>p = dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; P cap; s = sa\<rbrakk> \<Longrightarrow> ?Q26 s sa
 6. \<And>s. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s src_cap x. \<lbrakk>p = dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; P cap\<rbrakk> \<Longrightarrow> \<lbrace>?B29 s src_cap x ()\<rbrace> if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return () \<lbrace>\<lambda>ya. cte_wp_at (\<lambda>_. True) dest\<rbrace>
 2. \<And>s src_cap x. \<lbrakk>p = dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; P cap\<rbrakk> \<Longrightarrow> \<lbrace>?B28 s src_cap x\<rbrace> assert (x = NullCap) \<lbrace>?B29 s src_cap x\<rbrace>
 3. \<And>s src_cap. \<lbrakk>p = dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; P cap\<rbrakk> \<Longrightarrow> \<lbrace>?B27 s src_cap\<rbrace> get_cap dest \<lbrace>?B28 s src_cap\<rbrace>
 4. \<And>s. \<lbrakk>p = dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; P cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 s\<rbrace> get_cap src \<lbrace>?B27 s\<rbrace>
 5. \<And>s sa. \<lbrakk>p = dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; P cap; s = sa\<rbrakk> \<Longrightarrow> ?Q26 s sa
 6. \<And>s. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>p = dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; P cap; s = sa\<rbrakk> \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src sa \<longrightarrow> (\<forall>capb. cte_wp_at ((=) capb) dest sa \<longrightarrow> capb = NullCap \<longrightarrow> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> cte_wp_at (\<lambda>_. True) dest sa) \<and> (\<not> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap) \<longrightarrow> cte_wp_at (\<lambda>_. True) dest sa))
 2. \<And>s. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<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 <- update_cdt (\<lambda>cdt. cdt(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else cdt src));
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>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s src_cap x. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>?B82 s src_cap x ()\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>ya s. cte_wp_at P p s \<and> cte_wp_at (\<lambda>_. True) dest s\<rbrace>
 2. \<And>s src_cap x. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>?B81 s src_cap x\<rbrace> assert (x = NullCap) \<lbrace>?B82 s src_cap x\<rbrace>
 3. \<And>s src_cap. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>?B80 s src_cap\<rbrace> get_cap dest \<lbrace>?B81 s src_cap\<rbrace>
 4. \<And>s. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>?Q79 s\<rbrace> get_cap src \<lbrace>?B80 s\<rbrace>
 5. \<And>s sa. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s; s = sa\<rbrakk> \<Longrightarrow> ?Q79 s sa proof (prove)
goal (5 subgoals):
 1. \<And>s src_cap x. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>?B82 s src_cap x ()\<rbrace> if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return () \<lbrace>\<lambda>ya s. cte_wp_at P p s \<and> cte_wp_at (\<lambda>_. True) dest s\<rbrace>
 2. \<And>s src_cap x. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>?B81 s src_cap x\<rbrace> assert (x = NullCap) \<lbrace>?B82 s src_cap x\<rbrace>
 3. \<And>s src_cap. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>?B80 s src_cap\<rbrace> get_cap dest \<lbrace>?B81 s src_cap\<rbrace>
 4. \<And>s. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s\<rbrakk> \<Longrightarrow> \<lbrace>?Q79 s\<rbrace> get_cap src \<lbrace>?B80 s\<rbrace>
 5. \<And>s sa. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s; s = sa\<rbrakk> \<Longrightarrow> ?Q79 s sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>p \<noteq> dest; cte_wp_at (is_derived (cdt s) src cap) src s; valid_mdb s; valid_objs s; cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s; s = sa\<rbrakk> \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src sa \<longrightarrow> (\<forall>capb. cte_wp_at ((=) capb) dest sa \<longrightarrow> capb = NullCap \<longrightarrow> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> ((\<lambda>s. if p = src then P (max_free_index_update capa) else cte_wp_at P p s) and cte_wp_at (\<lambda>_. True) src) sa \<and> ((\<lambda>s. if dest = src then True else cte_wp_at (\<lambda>a. True) dest s) and cte_wp_at (\<lambda>_. True) src) sa) \<and> (\<not> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap) \<longrightarrow> cte_wp_at P p sa \<and> cte_wp_at (\<lambda>_. True) dest sa)) proof (prove)
goal (1 subgoal):
 1. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap)\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> capa = capb \<longrightarrow> caps_of_state sa dest = Some NullCap \<longrightarrow> (is_untyped_cap capb \<and> is_untyped_cap cap \<and> obj_ref_of capb = obj_ref_of cap \<and> cap_bits_untyped capb = cap_bits_untyped cap \<longrightarrow> P (max_free_index_update capb)) \<and> ((obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap) \<longrightarrow> P capb)) \<and> (p \<noteq> src \<longrightarrow> capa = capb \<longrightarrow> caps_of_state sa dest = Some NullCap \<longrightarrow> (is_untyped_cap capb \<and> is_untyped_cap cap \<and> obj_ref_of capb = obj_ref_of cap \<and> cap_bits_untyped capb = cap_bits_untyped cap \<longrightarrow> P capaa) \<and> ((obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap) \<longrightarrow> P capaa)) proof (prove)
goal (1 subgoal):
 1. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap); sa \<turnstile> capa\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> capa = capb \<longrightarrow> caps_of_state sa dest = Some NullCap \<longrightarrow> (is_untyped_cap capb \<and> is_untyped_cap cap \<and> obj_ref_of capb = obj_ref_of cap \<and> cap_bits_untyped capb = cap_bits_untyped cap \<longrightarrow> P (max_free_index_update capb)) \<and> ((obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap) \<longrightarrow> P capb)) \<and> (p \<noteq> src \<longrightarrow> capa = capb \<longrightarrow> caps_of_state sa dest = Some NullCap \<longrightarrow> (is_untyped_cap capb \<and> is_untyped_cap cap \<and> obj_ref_of capb = obj_ref_of cap \<and> cap_bits_untyped capb = cap_bits_untyped cap \<longrightarrow> P capaa) \<and> ((obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap) \<longrightarrow> P capaa)) proof (prove)
goal (4 subgoals):
 1. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap); sa \<turnstile> capa; p = src; capa = capb; caps_of_state sa dest = Some NullCap; is_untyped_cap capb \<and> is_untyped_cap cap \<and> obj_ref_of capb = obj_ref_of cap \<and> cap_bits_untyped capb = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P (max_free_index_update capb)
 2. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap); sa \<turnstile> capa; p = src; capa = capb; caps_of_state sa dest = Some NullCap; obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capb
 3. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap); sa \<turnstile> capa; p \<noteq> src; capa = capb; caps_of_state sa dest = Some NullCap; is_untyped_cap capb \<and> is_untyped_cap cap \<and> obj_ref_of capb = obj_ref_of cap \<and> cap_bits_untyped capb = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capaa
 4. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap); sa \<turnstile> capa; p \<noteq> src; capa = capb; caps_of_state sa dest = Some NullCap; obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capaa proof (prove)
goal (2 subgoals):
 1. \<And>sa capa capb. \<lbrakk>sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; is_derived (cdt sa) src cap capb; caps_of_state sa p = Some capa; is_untyped_cap capb; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; obj_ref_of capb = obj_ref_of cap; cap_bits_untyped capb = cap_bits_untyped cap; P (max_free_index_update capa)\<rbrakk> \<Longrightarrow> P capa
 2. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap); sa \<turnstile> capa; p \<noteq> src; capa = capb; caps_of_state sa dest = Some NullCap; obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capaa proof (prove)
goal (2 subgoals):
 1. \<And>sa capa capb. \<lbrakk>sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_objs sa; caps_of_state sa src = Some capb; caps_of_state sa p = Some capa; is_untyped_cap capb; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; obj_ref_of capb = obj_ref_of cap; cap_bits_untyped capb = cap_bits_untyped cap; P (max_free_index_update capa); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) sa) (cdt sa); cap \<noteq> NullCap; untyped_mdb (cdt sa) (caps_of_state sa); \<not> is_zombie capb; descendants_inc (cdt sa) (caps_of_state sa); cap \<noteq> IRQControlCap; no_mloop (cdt sa); cap_master_cap capb = cap_master_cap cap; untyped_inc (cdt sa) (caps_of_state sa); descendants_of src (cdt sa) = {}; ut_revocable (is_original_cap sa) (caps_of_state sa); is_master_reply_cap capb = is_reply_cap cap; irq_revocable (is_original_cap sa) (caps_of_state sa); is_derived_arch cap capb; reply_master_revocable (is_original_cap sa) (caps_of_state sa); \<not> is_reply_cap capb; \<not> is_master_reply_cap cap; reply_mdb (cdt sa) (caps_of_state sa); valid_arch_mdb (is_original_cap sa) (caps_of_state sa)\<rbrakk> \<Longrightarrow> P capa
 2. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap); sa \<turnstile> capa; p \<noteq> src; capa = capb; caps_of_state sa dest = Some NullCap; obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capaa proof (prove)
goal (2 subgoals):
 1. \<And>sa capa capb. \<lbrakk>sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_objs sa; caps_of_state sa p = Some capa; is_untyped_cap capb; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; obj_ref_of capb = obj_ref_of cap; cap_bits_untyped capb = cap_bits_untyped cap; P (max_free_index_update capa); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) sa) (cdt sa); cap \<noteq> NullCap; untyped_mdb (cdt sa) (caps_of_state sa); \<not> is_zombie capb; descendants_inc (cdt sa) (caps_of_state sa); cap \<noteq> IRQControlCap; no_mloop (cdt sa); cap_master_cap capb = cap_master_cap cap; untyped_inc (cdt sa) (caps_of_state sa); descendants_of src (cdt sa) = {}; ut_revocable (is_original_cap sa) (caps_of_state sa); is_master_reply_cap capb = is_reply_cap cap; irq_revocable (is_original_cap sa) (caps_of_state sa); is_derived_arch cap capb; reply_master_revocable (is_original_cap sa) (caps_of_state sa); \<not> is_reply_cap capb; \<not> is_master_reply_cap cap; reply_mdb (cdt sa) (caps_of_state sa); valid_arch_mdb (is_original_cap sa) (caps_of_state sa); (untyped_range capb \<subseteq> untyped_range capa \<or> untyped_range capa \<subseteq> untyped_range capb \<or> untyped_range capb \<inter> untyped_range capa = {}) \<and> (untyped_range capb \<subset> untyped_range capa \<longrightarrow> src \<in> descendants_of p (cdt sa) \<and> untyped_range capb \<inter> usable_untyped_range capa = {}) \<and> (untyped_range capa \<subset> untyped_range capb \<longrightarrow> p \<in> descendants_of src (cdt sa) \<and> untyped_range capa \<inter> usable_untyped_range capb = {}) \<and> (untyped_range capb = untyped_range capa \<longrightarrow> p \<in> descendants_of src (cdt sa) \<and> usable_untyped_range capb = {} \<or> src \<in> descendants_of p (cdt sa) \<and> usable_untyped_range capa = {} \<or> src = p)\<rbrakk> \<Longrightarrow> P capa
 2. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap); sa \<turnstile> capa; p \<noteq> src; capa = capb; caps_of_state sa dest = Some NullCap; obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capaa proof (prove)
goal (3 subgoals):
 1. \<And>sa dev deva devb rb bitsb f fa fb. \<lbrakk>p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_objs sa; caps_of_state sa p = Some (UntypedCap deva rb bitsb fa); P (UntypedCap deva rb bitsb (max_free_index bitsb)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) sa) (cdt sa); untyped_mdb (cdt sa) (caps_of_state sa); descendants_inc (cdt sa) (caps_of_state sa); no_mloop (cdt sa); cap_master_cap (UntypedCap dev rb bitsb f) = cap_master_cap (UntypedCap devb rb bitsb fb); untyped_inc (cdt sa) (caps_of_state sa); descendants_of src (cdt sa) = {}; ut_revocable (is_original_cap sa) (caps_of_state sa); irq_revocable (is_original_cap sa) (caps_of_state sa); is_derived_arch (UntypedCap devb rb bitsb fb) (UntypedCap dev rb bitsb f); reply_master_revocable (is_original_cap sa) (caps_of_state sa); reply_mdb (cdt sa) (caps_of_state sa); valid_arch_mdb (is_original_cap sa) (caps_of_state sa); cap = UntypedCap devb rb bitsb fb; fa < 2 ^ bitsb; is_aligned rb bitsb; bitsb < word_bits; src \<in> descendants_of p (cdt sa); \<not> rb + word_of_nat fa \<le> rb + 2 ^ bitsb - 1\<rbrakk> \<Longrightarrow> P (UntypedCap deva rb bitsb fa)
 2. \<And>sa dev deva devb r ra rb bits bitsa bitsb f fa fb. \<lbrakk>p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_objs sa; caps_of_state sa p = Some (UntypedCap deva rb bitsb fa); ra = rb; bitsa = bitsb; r = rb; bits = bitsb; P (UntypedCap deva rb bitsb (max_free_index bitsb)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) sa) (cdt sa); untyped_mdb (cdt sa) (caps_of_state sa); descendants_inc (cdt sa) (caps_of_state sa); no_mloop (cdt sa); cap_master_cap (UntypedCap dev rb bitsb f) = cap_master_cap (UntypedCap devb rb bitsb fb); untyped_inc (cdt sa) (caps_of_state sa); descendants_of src (cdt sa) = {}; ut_revocable (is_original_cap sa) (caps_of_state sa); irq_revocable (is_original_cap sa) (caps_of_state sa); is_derived_arch (UntypedCap devb rb bitsb fb) (UntypedCap dev rb bitsb f); reply_master_revocable (is_original_cap sa) (caps_of_state sa); reply_mdb (cdt sa) (caps_of_state sa); valid_arch_mdb (is_original_cap sa) (caps_of_state sa); cap = UntypedCap devb rb bitsb fb; \<not> fa < 2 ^ bitsb; is_aligned rb bitsb; bitsb < word_bits; src \<in> descendants_of p (cdt sa)\<rbrakk> \<Longrightarrow> P (UntypedCap deva rb bitsb fa)
 3. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap); sa \<turnstile> capa; p \<noteq> src; capa = capb; caps_of_state sa dest = Some NullCap; obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capaa proof (prove)
goal (4 subgoals):
 1. \<And>sa dev deva devb rb bitsb f fa fb. \<lbrakk>p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_objs sa; caps_of_state sa p = Some (UntypedCap deva rb bitsb fa); P (UntypedCap deva rb bitsb (max_free_index bitsb)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) sa) (cdt sa); untyped_mdb (cdt sa) (caps_of_state sa); descendants_inc (cdt sa) (caps_of_state sa); no_mloop (cdt sa); cap_master_cap (UntypedCap dev rb bitsb f) = cap_master_cap (UntypedCap devb rb bitsb fb); untyped_inc (cdt sa) (caps_of_state sa); descendants_of src (cdt sa) = {}; ut_revocable (is_original_cap sa) (caps_of_state sa); irq_revocable (is_original_cap sa) (caps_of_state sa); is_derived_arch (UntypedCap devb rb bitsb fb) (UntypedCap dev rb bitsb f); reply_master_revocable (is_original_cap sa) (caps_of_state sa); reply_mdb (cdt sa) (caps_of_state sa); valid_arch_mdb (is_original_cap sa) (caps_of_state sa); cap = UntypedCap devb rb bitsb fb; fa < 2 ^ bitsb; bitsb < word_bits; src \<in> descendants_of p (cdt sa); \<not> rb + word_of_nat fa \<le> rb + 2 ^ bitsb - 1\<rbrakk> \<Longrightarrow> word_of_nat fa \<le> 2 ^ bitsb - 1
 2. \<And>sa dev deva devb rb bitsb f fa fb. \<lbrakk>p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_objs sa; caps_of_state sa p = Some (UntypedCap deva rb bitsb fa); P (UntypedCap deva rb bitsb (max_free_index bitsb)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) sa) (cdt sa); untyped_mdb (cdt sa) (caps_of_state sa); descendants_inc (cdt sa) (caps_of_state sa); no_mloop (cdt sa); cap_master_cap (UntypedCap dev rb bitsb f) = cap_master_cap (UntypedCap devb rb bitsb fb); untyped_inc (cdt sa) (caps_of_state sa); descendants_of src (cdt sa) = {}; ut_revocable (is_original_cap sa) (caps_of_state sa); irq_revocable (is_original_cap sa) (caps_of_state sa); is_derived_arch (UntypedCap devb rb bitsb fb) (UntypedCap dev rb bitsb f); reply_master_revocable (is_original_cap sa) (caps_of_state sa); reply_mdb (cdt sa) (caps_of_state sa); valid_arch_mdb (is_original_cap sa) (caps_of_state sa); cap = UntypedCap devb rb bitsb fb; fa < 2 ^ bitsb; bitsb < word_bits; src \<in> descendants_of p (cdt sa); \<not> rb + word_of_nat fa \<le> rb + 2 ^ bitsb - 1; rb + word_of_nat fa \<le> rb + (2 ^ bitsb - 1)\<rbrakk> \<Longrightarrow> P (UntypedCap deva rb bitsb fa)
 3. \<And>sa dev deva devb r ra rb bits bitsa bitsb f fa fb. \<lbrakk>p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_objs sa; caps_of_state sa p = Some (UntypedCap deva rb bitsb fa); ra = rb; bitsa = bitsb; r = rb; bits = bitsb; P (UntypedCap deva rb bitsb (max_free_index bitsb)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) sa) (cdt sa); untyped_mdb (cdt sa) (caps_of_state sa); descendants_inc (cdt sa) (caps_of_state sa); no_mloop (cdt sa); cap_master_cap (UntypedCap dev rb bitsb f) = cap_master_cap (UntypedCap devb rb bitsb fb); untyped_inc (cdt sa) (caps_of_state sa); descendants_of src (cdt sa) = {}; ut_revocable (is_original_cap sa) (caps_of_state sa); irq_revocable (is_original_cap sa) (caps_of_state sa); is_derived_arch (UntypedCap devb rb bitsb fb) (UntypedCap dev rb bitsb f); reply_master_revocable (is_original_cap sa) (caps_of_state sa); reply_mdb (cdt sa) (caps_of_state sa); valid_arch_mdb (is_original_cap sa) (caps_of_state sa); cap = UntypedCap devb rb bitsb fb; \<not> fa < 2 ^ bitsb; is_aligned rb bitsb; bitsb < word_bits; src \<in> descendants_of p (cdt sa)\<rbrakk> \<Longrightarrow> P (UntypedCap deva rb bitsb fa)
 4. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap); sa \<turnstile> capa; p \<noteq> src; capa = capb; caps_of_state sa dest = Some NullCap; obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capaa proof (prove)
goal (3 subgoals):
 1. \<And>sa dev deva devb rb bitsb f fa fb. \<lbrakk>p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_objs sa; caps_of_state sa p = Some (UntypedCap deva rb bitsb fa); P (UntypedCap deva rb bitsb (max_free_index bitsb)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) sa) (cdt sa); untyped_mdb (cdt sa) (caps_of_state sa); descendants_inc (cdt sa) (caps_of_state sa); no_mloop (cdt sa); cap_master_cap (UntypedCap dev rb bitsb f) = cap_master_cap (UntypedCap devb rb bitsb fb); untyped_inc (cdt sa) (caps_of_state sa); descendants_of src (cdt sa) = {}; ut_revocable (is_original_cap sa) (caps_of_state sa); irq_revocable (is_original_cap sa) (caps_of_state sa); is_derived_arch (UntypedCap devb rb bitsb fb) (UntypedCap dev rb bitsb f); reply_master_revocable (is_original_cap sa) (caps_of_state sa); reply_mdb (cdt sa) (caps_of_state sa); valid_arch_mdb (is_original_cap sa) (caps_of_state sa); cap = UntypedCap devb rb bitsb fb; fa < 2 ^ bitsb; bitsb < word_bits; src \<in> descendants_of p (cdt sa); \<not> rb + word_of_nat fa \<le> rb + 2 ^ bitsb - 1; rb + word_of_nat fa \<le> rb + (2 ^ bitsb - 1)\<rbrakk> \<Longrightarrow> P (UntypedCap deva rb bitsb fa)
 2. \<And>sa dev deva devb r ra rb bits bitsa bitsb f fa fb. \<lbrakk>p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_objs sa; caps_of_state sa p = Some (UntypedCap deva rb bitsb fa); ra = rb; bitsa = bitsb; r = rb; bits = bitsb; P (UntypedCap deva rb bitsb (max_free_index bitsb)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) sa) (cdt sa); untyped_mdb (cdt sa) (caps_of_state sa); descendants_inc (cdt sa) (caps_of_state sa); no_mloop (cdt sa); cap_master_cap (UntypedCap dev rb bitsb f) = cap_master_cap (UntypedCap devb rb bitsb fb); untyped_inc (cdt sa) (caps_of_state sa); descendants_of src (cdt sa) = {}; ut_revocable (is_original_cap sa) (caps_of_state sa); irq_revocable (is_original_cap sa) (caps_of_state sa); is_derived_arch (UntypedCap devb rb bitsb fb) (UntypedCap dev rb bitsb f); reply_master_revocable (is_original_cap sa) (caps_of_state sa); reply_mdb (cdt sa) (caps_of_state sa); valid_arch_mdb (is_original_cap sa) (caps_of_state sa); cap = UntypedCap devb rb bitsb fb; \<not> fa < 2 ^ bitsb; is_aligned rb bitsb; bitsb < word_bits; src \<in> descendants_of p (cdt sa)\<rbrakk> \<Longrightarrow> P (UntypedCap deva rb bitsb fa)
 3. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap); sa \<turnstile> capa; p \<noteq> src; capa = capb; caps_of_state sa dest = Some NullCap; obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capaa proof (prove)
goal (2 subgoals):
 1. \<And>sa dev deva devb r ra rb bits bitsa bitsb f fa fb. \<lbrakk>p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_objs sa; caps_of_state sa p = Some (UntypedCap deva rb bitsb fa); ra = rb; bitsa = bitsb; r = rb; bits = bitsb; P (UntypedCap deva rb bitsb (max_free_index bitsb)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) sa) (cdt sa); untyped_mdb (cdt sa) (caps_of_state sa); descendants_inc (cdt sa) (caps_of_state sa); no_mloop (cdt sa); cap_master_cap (UntypedCap dev rb bitsb f) = cap_master_cap (UntypedCap devb rb bitsb fb); untyped_inc (cdt sa) (caps_of_state sa); descendants_of src (cdt sa) = {}; ut_revocable (is_original_cap sa) (caps_of_state sa); irq_revocable (is_original_cap sa) (caps_of_state sa); is_derived_arch (UntypedCap devb rb bitsb fb) (UntypedCap dev rb bitsb f); reply_master_revocable (is_original_cap sa) (caps_of_state sa); reply_mdb (cdt sa) (caps_of_state sa); valid_arch_mdb (is_original_cap sa) (caps_of_state sa); cap = UntypedCap devb rb bitsb fb; \<not> fa < 2 ^ bitsb; is_aligned rb bitsb; bitsb < word_bits; src \<in> descendants_of p (cdt sa)\<rbrakk> \<Longrightarrow> P (UntypedCap deva rb bitsb fa)
 2. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap); sa \<turnstile> capa; p \<noteq> src; capa = capb; caps_of_state sa dest = Some NullCap; obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capaa proof (prove)
goal (2 subgoals):
 1. \<And>sa dev deva devb r ra rb bits bitsa bitsb f fa fb. \<lbrakk>p \<noteq> src; p \<noteq> dest; valid_objs sa; ra = rb; bitsa = bitsb; r = rb; bits = bitsb; P (UntypedCap deva rb bitsb (max_free_index bitsb)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) sa) (cdt sa); untyped_mdb (cdt sa) (caps_of_state sa); descendants_inc (cdt sa) (caps_of_state sa); no_mloop (cdt sa); cap_master_cap (UntypedCap dev rb bitsb f) = cap_master_cap (UntypedCap devb rb bitsb fb); untyped_inc (cdt sa) (caps_of_state sa); descendants_of src (cdt sa) = {}; ut_revocable (is_original_cap sa) (caps_of_state sa); irq_revocable (is_original_cap sa) (caps_of_state sa); is_derived_arch (UntypedCap devb rb bitsb fb) (UntypedCap dev rb bitsb f); reply_master_revocable (is_original_cap sa) (caps_of_state sa); reply_mdb (cdt sa) (caps_of_state sa); valid_arch_mdb (is_original_cap sa) (caps_of_state sa); cap = UntypedCap devb rb bitsb fb; \<not> fa < 2 ^ bitsb; is_aligned rb bitsb; bitsb < word_bits; src \<in> descendants_of p (cdt sa); sa \<turnstile> NullCap; sa \<turnstile> UntypedCap deva rb bitsb fa\<rbrakk> \<Longrightarrow> P (UntypedCap deva rb bitsb fa)
 2. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap); sa \<turnstile> capa; p \<noteq> src; capa = capb; caps_of_state sa dest = Some NullCap; obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capaa proof (prove)
goal (1 subgoal):
 1. \<And>sa capa capaa capb. \<lbrakk>p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capa; is_derived (cdt sa) src cap capa; caps_of_state sa p = Some capaa; P (masked_as_full capaa cap); sa \<turnstile> capa; p \<noteq> src; capa = capb; caps_of_state sa dest = Some NullCap; obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capaa proof (prove)
goal (1 subgoal):
 1. \<And>sa capa capb. \<lbrakk>sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; obj_ref_of capb = obj_ref_of cap \<longrightarrow> is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; is_derived (cdt sa) src cap capb; caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa)\<rbrakk> \<Longrightarrow> P capa proof (prove)
goal (2 subgoals):
 1. \<And>sa capa capb. \<lbrakk>sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; is_derived (cdt sa) src cap capb; caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa)\<rbrakk> \<Longrightarrow> obj_ref_of capb = obj_ref_of cap
 2. \<And>sa capa capb. \<lbrakk>sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; is_derived (cdt sa) src cap capb; caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa); obj_ref_of capb = obj_ref_of cap; is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capa proof (prove)
goal (3 subgoals):
 1. \<And>sa capa capb. \<lbrakk>caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa); sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; is_untyped_cap capb; cap \<noteq> NullCap; \<not> is_zombie capb; cap \<noteq> IRQControlCap; cap_master_cap capb = cap_master_cap cap; descendants_of src (cdt sa) = {}; is_master_reply_cap capb = is_reply_cap cap; is_derived_arch cap capb; \<not> is_reply_cap capb; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> obj_ref_of capb = obj_ref_of cap
 2. \<And>sa capa capb. \<lbrakk>caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa); sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; \<not> is_untyped_cap capb; cap \<noteq> NullCap; \<not> is_zombie capb; cap \<noteq> IRQControlCap; cap_master_cap capb = cap_master_cap cap; (cap_badge capb, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capb = is_reply_cap cap; is_derived_arch cap capb; \<not> is_reply_cap capb; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> obj_ref_of capb = obj_ref_of cap
 3. \<And>sa capa capb. \<lbrakk>sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; is_derived (cdt sa) src cap capb; caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa); obj_ref_of capb = obj_ref_of cap; is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capa proof (prove)
goal (2 subgoals):
 1. \<And>sa capa capb. \<lbrakk>caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa); sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; \<not> is_untyped_cap capb; cap \<noteq> NullCap; \<not> is_zombie capb; cap \<noteq> IRQControlCap; cap_master_cap capb = cap_master_cap cap; (cap_badge capb, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capb = is_reply_cap cap; is_derived_arch cap capb; \<not> is_reply_cap capb; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> obj_ref_of capb = obj_ref_of cap
 2. \<And>sa capa capb. \<lbrakk>sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; is_derived (cdt sa) src cap capb; caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa); obj_ref_of capb = obj_ref_of cap; is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capa proof (prove)
goal (1 subgoal):
 1. \<And>sa capa capb. \<lbrakk>sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; is_derived (cdt sa) src cap capb; caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa); obj_ref_of capb = obj_ref_of cap; is_untyped_cap capb \<longrightarrow> cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capa proof (prove)
goal (2 subgoals):
 1. \<And>sa capa capb. \<lbrakk>sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; is_derived (cdt sa) src cap capb; caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa); obj_ref_of capb = obj_ref_of cap\<rbrakk> \<Longrightarrow> is_untyped_cap capb
 2. \<And>sa capa capb. \<lbrakk>sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; is_derived (cdt sa) src cap capb; caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa); obj_ref_of capb = obj_ref_of cap; is_untyped_cap capb; cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capa proof (prove)
goal (2 subgoals):
 1. \<And>sa capa capb. \<lbrakk>caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa); obj_ref_of capb = obj_ref_of cap; sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; \<not> is_untyped_cap capb; cap \<noteq> NullCap; \<not> is_zombie capb; cap \<noteq> IRQControlCap; cap_master_cap capb = cap_master_cap cap; (cap_badge capb, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capb = is_reply_cap cap; is_derived_arch cap capb; \<not> is_reply_cap capb; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> False
 2. \<And>sa capa capb. \<lbrakk>sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; is_derived (cdt sa) src cap capb; caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa); obj_ref_of capb = obj_ref_of cap; is_untyped_cap capb; cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capa proof (prove)
goal (2 subgoals):
 1. \<And>sa capb dev deva bitsa f fa. \<lbrakk>caps_of_state sa p = Some (UntypedCap dev (obj_ref_of capb) bitsa f); P (UntypedCap dev (obj_ref_of capb) bitsa (max_free_index bitsa)); sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; \<forall>dev r bits f. capb \<noteq> UntypedCap dev r bits f; \<forall>r b n. capb \<noteq> Zombie r b n; cap_master_cap capb = UntypedCap deva (obj_ref_of capb) bitsa 0; cap_badge capb = None; \<forall>x R. capb \<noteq> ReplyCap x True R; is_derived_arch (UntypedCap deva (obj_ref_of capb) bitsa fa) capb; \<forall>x R. capb \<noteq> ReplyCap x False R; cap = UntypedCap deva (obj_ref_of capb) bitsa fa\<rbrakk> \<Longrightarrow> False
 2. \<And>sa capa capb. \<lbrakk>sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; is_derived (cdt sa) src cap capb; caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa); obj_ref_of capb = obj_ref_of cap; is_untyped_cap capb; cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capa proof (prove)
goal (1 subgoal):
 1. \<And>sa capa capb. \<lbrakk>sa \<turnstile> capb; p \<noteq> src; caps_of_state sa dest = Some NullCap; p \<noteq> dest; valid_mdb sa; valid_objs sa; caps_of_state sa src = Some capb; is_derived (cdt sa) src cap capb; caps_of_state sa p = Some capa; is_untyped_cap capa; is_untyped_cap cap; obj_ref_of capa = obj_ref_of cap; cap_bits_untyped capa = cap_bits_untyped cap; P (max_free_index_update capa); obj_ref_of capb = obj_ref_of cap; is_untyped_cap capb; cap_bits_untyped capb \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> P capa proof (prove)
goal:
No subgoals!