theory Interrupt_AI

lemma cap_delete_one_still_derived:
  "\<lbrace>\<lambda>s. cte_wp_at (is_derived (cdt s) p' cap) p' s \<and> p \<noteq> p' \<and> valid_mdb s\<rbrace>
     cap_delete_one p
   \<lbrace>\<lambda>rv s. cte_wp_at (is_derived (cdt s) p' cap) p' s\<rbrace>" apply (simp add: cap_delete_one_def empty_slot_def unless_def
                   cte_wp_at_caps_of_state set_cdt_def) apply (wp hoare_vcg_ex_lift) apply (simp split del:if_split) apply (wp hoare_vcg_ex_lift get_cap_wp hoare_vcg_all_lift
            hoare_vcg_disj_lift
               | simp only: cte_wp_at_caps_of_state imp_conv_disj
                            cdt_update.caps_of_state_update
                            revokable_update.caps_of_state_update
               | simp)+ apply (simp add: is_final_cap_def | wp)+ apply (rule get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state if_apply_def2
             split del: if_split) apply (rule_tac x=capa in exI) apply (clarsimp simp only: is_derived_def simp_thms
                      split: if_split_asm) apply clarsimp apply (subst mdb_empty_abs.descendants[unfolded fun_upd_def]) apply (rule mdb_empty_abs.intro) apply (rule vmdb_abs.intro) apply simp apply simp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (is_derived (cdt s) p' cap) p' s \<and> p \<noteq> p' \<and> valid_mdb s\<rbrace> cap_delete_one p \<lbrace>\<lambda>rv s. cte_wp_at (is_derived (cdt s) p' cap) p' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>capa. caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa) \<and> p \<noteq> p' \<and> valid_mdb s\<rbrace> do cap <- get_cap p;
when (cap \<noteq> NullCap) (do final <- is_final_cap cap;
y <- fast_finalise cap final;
cap <- get_cap p;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s p);
cdt <- gets cdt;
y <- do s <- get;
put (s\<lparr>cdt := (\<lambda>pa. if cdt pa = Some p then cdt p else cdt pa)(p := None)\<rparr>)
od;
y <- do_extended_op (empty_slot_ext p slot_p);
y <- set_original p False;
y <- set_cap NullCap p;
post_cap_deletion NullCap
od
od)
od \<lbrace>\<lambda>rv s. \<exists>capa. caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>capa capaa final y capb slot_p cdta ya s f. \<lbrakk>capaa \<noteq> NullCap; capb \<noteq> NullCap\<rbrakk> \<Longrightarrow> (((caps_of_state (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(p := False)\<rparr>))(p \<mapsto> NullCap)) p' = Some capa \<and> is_derived (cdt (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(p := False)\<rparr>)) p' cap capa) = (((caps_of_state (s\<lparr>is_original_cap := (is_original_cap s)(p := False)\<rparr>))(p \<mapsto> NullCap)) p' = Some capa \<and> is_derived (cdt (s\<lparr>is_original_cap := (is_original_cap s)(p := False)\<rparr>)) p' cap capa)
 2. \<And>capa capaa final y capb slot_p cdta. \<lbrakk>capaa \<noteq> NullCap; capb \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B10 capa capaa final y capb slot_p cdta\<rbrace> do s <- get;
put (s\<lparr>cdt := (\<lambda>pa. if cdta pa = Some p then cdta p else cdta pa)(p := None)\<rparr>)
od \<lbrace>\<lambda>ya s. ((caps_of_state (s\<lparr>is_original_cap := (is_original_cap s)(p := False)\<rparr>))(p \<mapsto> NullCap)) p' = Some capa \<and> is_derived (cdt (s\<lparr>is_original_cap := (is_original_cap s)(p := False)\<rparr>)) p' cap capa\<rbrace>
 3. \<And>cap capa final y capb slot_p. \<lbrakk>capa \<noteq> NullCap; capb \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap capa final y capb slot_p\<rbrace> gets cdt \<lbrace>?B10 cap capa final y capb slot_p\<rbrace>
 4. \<And>cap capa final y capb. \<lbrakk>capa \<noteq> NullCap; capb \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R7 cap capa final y capb\<rbrace> gets (\<lambda>s. cdt s p) \<lbrace>?B9 cap capa final y capb\<rbrace>
 5. \<And>capa capaa final y. capaa \<noteq> NullCap \<Longrightarrow> \<lbrace>?B5 capa capaa final y\<rbrace> get_cap p \<lbrace>\<lambda>capb s. (capb = NullCap \<longrightarrow> caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa) \<and> (capb \<noteq> NullCap \<longrightarrow> ?R7 capa capaa final y capb s)\<rbrace>
 6. \<And>cap capa final. capa \<noteq> NullCap \<Longrightarrow> \<lbrace>?B4 cap capa final\<rbrace> fast_finalise capa final \<lbrace>?B5 cap capa final\<rbrace>
 7. \<And>cap capa. capa \<noteq> NullCap \<Longrightarrow> \<lbrace>?Q3 cap capa\<rbrace> is_final_cap capa \<lbrace>?B4 cap capa\<rbrace>
 8. \<And>capa. \<lbrace>?P1 capa\<rbrace> get_cap p \<lbrace>\<lambda>capaa. if capaa \<noteq> NullCap then ?Q3 capa capaa else (\<lambda>s. caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa)\<rbrace>
 9. \<And>s. (\<exists>capa. caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa) \<and> p \<noteq> p' \<and> valid_mdb s \<Longrightarrow> \<exists>x. ?P1 x s proof (prove)
goal (8 subgoals):
 1. \<And>capa capaa final y capb slot_p cdta. \<lbrakk>capaa \<noteq> NullCap; capb \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B10 capa capaa final y capb slot_p cdta\<rbrace> do s <- get;
put (s\<lparr>cdt := (\<lambda>pa. if cdta pa = Some p then cdta p else cdta pa)(p := None)\<rparr>)
od \<lbrace>\<lambda>ya s. ((caps_of_state (s\<lparr>is_original_cap := (is_original_cap s)(p := False)\<rparr>))(p \<mapsto> NullCap)) p' = Some capa \<and> is_derived (cdt (s\<lparr>is_original_cap := (is_original_cap s)(p := False)\<rparr>)) p' cap capa\<rbrace>
 2. \<And>cap capa final y capb slot_p. \<lbrakk>capa \<noteq> NullCap; capb \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap capa final y capb slot_p\<rbrace> gets cdt \<lbrace>?B10 cap capa final y capb slot_p\<rbrace>
 3. \<And>cap capa final y capb. \<lbrakk>capa \<noteq> NullCap; capb \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R7 cap capa final y capb\<rbrace> gets (\<lambda>s. cdt s p) \<lbrace>?B9 cap capa final y capb\<rbrace>
 4. \<And>capa capaa final y. capaa \<noteq> NullCap \<Longrightarrow> \<lbrace>?B5 capa capaa final y\<rbrace> get_cap p \<lbrace>\<lambda>capb s. (capb = NullCap \<longrightarrow> caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa) \<and> (capb \<noteq> NullCap \<longrightarrow> ?R7 capa capaa final y capb s)\<rbrace>
 5. \<And>cap capa final. capa \<noteq> NullCap \<Longrightarrow> \<lbrace>?B4 cap capa final\<rbrace> fast_finalise capa final \<lbrace>?B5 cap capa final\<rbrace>
 6. \<And>cap capa. capa \<noteq> NullCap \<Longrightarrow> \<lbrace>?Q3 cap capa\<rbrace> is_final_cap capa \<lbrace>?B4 cap capa\<rbrace>
 7. \<And>capa. \<lbrace>?P1 capa\<rbrace> get_cap p \<lbrace>\<lambda>capaa. if capaa \<noteq> NullCap then ?Q3 capa capaa else (\<lambda>s. caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa)\<rbrace>
 8. \<And>s. (\<exists>capa. caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa) \<and> p \<noteq> p' \<and> valid_mdb s \<Longrightarrow> \<exists>x. ?P1 x s proof (prove)
goal (4 subgoals):
 1. \<And>cap capa x. capa \<noteq> NullCap \<Longrightarrow> \<lbrace>?P73 cap capa x\<rbrace> is_final_cap capa \<lbrace>\<lambda>rv s. caps_of_state s p \<noteq> Some x\<rbrace>
 2. \<And>capa capaa x. capaa \<noteq> NullCap \<Longrightarrow> \<lbrace>?P'73 capa capaa x\<rbrace> is_final_cap capaa \<lbrace>\<lambda>rv s. (x \<noteq> NullCap \<or> caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa) \<and> (\<not> x \<noteq> NullCap \<or> ((caps_of_state s)(p \<mapsto> NullCap)) p' = Some capa \<and> is_derived ((\<lambda>pa. if cdt s pa = Some p then cdt s p else cdt s pa)(p := None)) p' cap capa)\<rbrace>
 3. \<And>capa. \<lbrace>?P1 capa\<rbrace> get_cap p \<lbrace>\<lambda>capaa. if capaa \<noteq> NullCap then \<lambda>s. \<forall>x. ?P73 capa capaa x s \<or> ?P'73 capa capaa x s else (\<lambda>s. caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa)\<rbrace>
 4. \<And>s. (\<exists>capa. caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa) \<and> p \<noteq> p' \<and> valid_mdb s \<Longrightarrow> \<exists>x. ?P1 x s proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrace>?P1 capa\<rbrace> get_cap p \<lbrace>\<lambda>capaa. if capaa \<noteq> NullCap then \<lambda>s. \<forall>x. caps_of_state s p = Some x \<longrightarrow> (p' = p \<longrightarrow> (x = NullCap \<longrightarrow> NullCap = capa \<and> is_derived (cdt s) p cap capa) \<and> (x = NullCap \<or> NullCap = capa \<and> is_derived (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) p cap capa)) \<and> (p' \<noteq> p \<longrightarrow> (x = NullCap \<longrightarrow> caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa) \<and> (x = NullCap \<or> caps_of_state s p' = Some capa \<and> is_derived (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) p' cap capa)) else (\<lambda>s. caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa)\<rbrace>
 2. \<And>s. (\<exists>capa. caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa) \<and> p \<noteq> p' \<and> valid_mdb s \<Longrightarrow> \<exists>x. ?P1 x s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>capa. caps_of_state s p' = Some capa \<and> is_derived (cdt s) p' cap capa) \<and> p \<noteq> p' \<and> valid_mdb s \<Longrightarrow> \<exists>x. \<forall>capa. cte_wp_at ((=) capa) p s \<longrightarrow> (if capa \<noteq> NullCap then \<lambda>s. \<forall>xa. caps_of_state s p = Some xa \<longrightarrow> (p' = p \<longrightarrow> (xa = NullCap \<longrightarrow> NullCap = x \<and> is_derived (cdt s) p cap x) \<and> (xa = NullCap \<or> NullCap = x \<and> is_derived (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) p cap x)) \<and> (p' \<noteq> p \<longrightarrow> (xa = NullCap \<longrightarrow> caps_of_state s p' = Some x \<and> is_derived (cdt s) p' cap x) \<and> (xa = NullCap \<or> caps_of_state s p' = Some x \<and> is_derived (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) p' cap x)) else (\<lambda>s. caps_of_state s p' = Some x \<and> is_derived (cdt s) p' cap x)) s proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; is_derived (cdt s) p' cap capa\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>capb. caps_of_state s p = Some capb \<longrightarrow> (capb \<noteq> NullCap \<longrightarrow> capa = x \<and> is_derived (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) p' cap x) \<and> (capb = NullCap \<longrightarrow> capa = x \<and> is_derived (cdt s) p' cap x) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; is_derived (cdt s) p' cap capa\<rbrakk> \<Longrightarrow> \<forall>capb. caps_of_state s p = Some capb \<longrightarrow> (capb \<noteq> NullCap \<longrightarrow> capa = capa \<and> is_derived (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) p' cap capa) \<and> (capb = NullCap \<longrightarrow> capa = capa \<and> is_derived (cdt s) p' cap capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; descendants_of p' (cdt s) = {}; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa\<rbrakk> \<Longrightarrow> (capaa \<noteq> NullCap \<longrightarrow> (if True then descendants_of p' (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) = {} else (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False)) \<and> (capaa = NullCap \<longrightarrow> (if True then True else (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False))
 2. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; \<not> is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa\<rbrakk> \<Longrightarrow> (capaa \<noteq> NullCap \<longrightarrow> (if False then descendants_of p' (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) = {} else True)) \<and> (capaa = NullCap \<longrightarrow> (if False then descendants_of p' (cdt s) = {} else True)) proof (prove)
goal (2 subgoals):
 1. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; descendants_of p' (cdt s) = {}; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa; capaa \<noteq> NullCap\<rbrakk> \<Longrightarrow> descendants_of p' (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) = {}
 2. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; \<not> is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa\<rbrakk> \<Longrightarrow> (capaa \<noteq> NullCap \<longrightarrow> (if False then descendants_of p' (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) = {} else True)) \<and> (capaa = NullCap \<longrightarrow> (if False then descendants_of p' (cdt s) = {} else True)) proof (prove)
goal (3 subgoals):
 1. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; descendants_of p' (cdt s) = {}; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa; capaa \<noteq> NullCap\<rbrakk> \<Longrightarrow> mdb_empty_abs s
 2. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; descendants_of p' (cdt s) = {}; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa; capaa \<noteq> NullCap\<rbrakk> \<Longrightarrow> (if p' = p then {} else descendants_of p' (cdt s) - {p}) = {}
 3. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; \<not> is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa\<rbrakk> \<Longrightarrow> (capaa \<noteq> NullCap \<longrightarrow> (if False then descendants_of p' (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) = {} else True)) \<and> (capaa = NullCap \<longrightarrow> (if False then descendants_of p' (cdt s) = {} else True)) proof (prove)
goal (3 subgoals):
 1. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; descendants_of p' (cdt s) = {}; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa; capaa \<noteq> NullCap\<rbrakk> \<Longrightarrow> vmdb_abs s
 2. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; descendants_of p' (cdt s) = {}; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa; capaa \<noteq> NullCap\<rbrakk> \<Longrightarrow> (if p' = p then {} else descendants_of p' (cdt s) - {p}) = {}
 3. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; \<not> is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa\<rbrakk> \<Longrightarrow> (capaa \<noteq> NullCap \<longrightarrow> (if False then descendants_of p' (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) = {} else True)) \<and> (capaa = NullCap \<longrightarrow> (if False then descendants_of p' (cdt s) = {} else True)) proof (prove)
goal (3 subgoals):
 1. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; descendants_of p' (cdt s) = {}; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa; capaa \<noteq> NullCap\<rbrakk> \<Longrightarrow> valid_mdb s
 2. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; descendants_of p' (cdt s) = {}; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa; capaa \<noteq> NullCap\<rbrakk> \<Longrightarrow> (if p' = p then {} else descendants_of p' (cdt s) - {p}) = {}
 3. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; \<not> is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa\<rbrakk> \<Longrightarrow> (capaa \<noteq> NullCap \<longrightarrow> (if False then descendants_of p' (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) = {} else True)) \<and> (capaa = NullCap \<longrightarrow> (if False then descendants_of p' (cdt s) = {} else True)) proof (prove)
goal (2 subgoals):
 1. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; descendants_of p' (cdt s) = {}; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa; capaa \<noteq> NullCap\<rbrakk> \<Longrightarrow> (if p' = p then {} else descendants_of p' (cdt s) - {p}) = {}
 2. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; \<not> is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa\<rbrakk> \<Longrightarrow> (capaa \<noteq> NullCap \<longrightarrow> (if False then descendants_of p' (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) = {} else True)) \<and> (capaa = NullCap \<longrightarrow> (if False then descendants_of p' (cdt s) = {} else True)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa capaa. \<lbrakk>p \<noteq> p'; valid_mdb s; caps_of_state s p' = Some capa; \<not> is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; caps_of_state s p = Some capaa\<rbrakk> \<Longrightarrow> (capaa \<noteq> NullCap \<longrightarrow> (if False then descendants_of p' (\<lambda>a. if a = p then None else if cdt s a = Some p then cdt s p else cdt s a) = {} else True)) \<and> (capaa = NullCap \<longrightarrow> (if False then descendants_of p' (cdt s) = {} else True)) proof (prove)
goal:
No subgoals!