theory CSpaceInv_AI

lemma replace_cap_valid_pspace:
  "\<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (replaceable s p cap) p s
          \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv. valid_pspace\<rbrace>" apply (simp only: replaceable_def cte_wp_at_disj
                    conj_disj_distribL conj_disj_distribR) apply (rule hoare_strengthen_post) apply (rule hoare_vcg_disj_lift) apply (rule hoare_pre, rule set_cap_same_valid_pspace) apply simp apply (rule hoare_vcg_disj_lift) apply (cases "cap = cap.NullCap") apply simp apply (rule hoare_pre, rule delete_duplicate_valid_pspace) apply (fastforce simp: cte_wp_at_caps_of_state) apply (simp add: cte_wp_at_caps_of_state) apply (rule hoare_pre, rule set_cap_valid_pspace) apply (clarsimp simp: cte_wp_at_def) apply (clarsimp simp: ex_zombie_refs_def2 split: if_split_asm) apply (erule(3) final_cap_duplicate,
            erule subsetD, erule obj_ref_is_gen_obj_ref,
            erule subsetD, erule obj_ref_is_gen_obj_ref,
            erule obj_ref_is_gen_obj_ref)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (replaceable s p cap) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. capa = cap) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s \<or> valid_pspace s \<and> cte_wp_at (\<lambda>capa. \<not> is_final_cap' capa s \<and> cap = NullCap \<and> replaceable_non_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s \<or> valid_pspace s \<and> cte_wp_at (\<lambda>capa. is_final_cap' capa s \<and> (\<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>p'. p' \<in> cte_refs capa (interrupt_irq_node s) \<and> p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> p' \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs capa \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa) \<and> (is_master_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (is_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap capa \<longrightarrow> tcb_cap_valid capa p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa) \<and> replaceable_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_pspace\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. capa = cap) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s \<or> valid_pspace s \<and> cte_wp_at (\<lambda>capa. \<not> is_final_cap' capa s \<and> cap = NullCap \<and> replaceable_non_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s \<or> valid_pspace s \<and> cte_wp_at (\<lambda>capa. is_final_cap' capa s \<and> (\<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>p'. p' \<in> cte_refs capa (interrupt_irq_node s) \<and> p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> p' \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs capa \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa) \<and> (is_master_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (is_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap capa \<longrightarrow> tcb_cap_valid capa p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa) \<and> replaceable_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> valid_pspace s proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. capa = cap) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q3\<rbrace>
 2. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. \<not> is_final_cap' capa s \<and> cap = NullCap \<and> replaceable_non_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s \<or> valid_pspace s \<and> cte_wp_at (\<lambda>capa. is_final_cap' capa s \<and> (\<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>p'. p' \<in> cte_refs capa (interrupt_irq_node s) \<and> p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> p' \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs capa \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa) \<and> (is_master_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (is_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap capa \<longrightarrow> tcb_cap_valid capa p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa) \<and> replaceable_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q'3\<rbrace>
 3. \<And>rv s. ?Q3 rv s \<or> ?Q'3 rv s \<Longrightarrow> valid_pspace s proof (prove)
goal (3 subgoals):
 1. \<And>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. capa = cap) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap) p and valid_pspace) s
 2. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. \<not> is_final_cap' capa s \<and> cap = NullCap \<and> replaceable_non_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s \<or> valid_pspace s \<and> cte_wp_at (\<lambda>capa. is_final_cap' capa s \<and> (\<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>p'. p' \<in> cte_refs capa (interrupt_irq_node s) \<and> p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> p' \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs capa \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa) \<and> (is_master_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (is_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap capa \<longrightarrow> tcb_cap_valid capa p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa) \<and> replaceable_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q'3\<rbrace>
 3. \<And>rv s. valid_pspace s \<or> ?Q'3 rv s \<Longrightarrow> valid_pspace s proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. \<not> is_final_cap' capa s \<and> cap = NullCap \<and> replaceable_non_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s \<or> valid_pspace s \<and> cte_wp_at (\<lambda>capa. is_final_cap' capa s \<and> (\<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>p'. p' \<in> cte_refs capa (interrupt_irq_node s) \<and> p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> p' \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs capa \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa) \<and> (is_master_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (is_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap capa \<longrightarrow> tcb_cap_valid capa p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa) \<and> replaceable_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q'3\<rbrace>
 2. \<And>rv s. valid_pspace s \<or> ?Q'3 rv s \<Longrightarrow> valid_pspace s proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. \<not> is_final_cap' capa s \<and> cap = NullCap \<and> replaceable_non_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q10\<rbrace>
 2. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. is_final_cap' capa s \<and> (\<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>p'. p' \<in> cte_refs capa (interrupt_irq_node s) \<and> p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> p' \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs capa \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa) \<and> (is_master_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (is_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap capa \<longrightarrow> tcb_cap_valid capa p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa) \<and> replaceable_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q'10\<rbrace>
 3. \<And>rv s. valid_pspace s \<or> ?Q10 rv s \<or> ?Q'10 rv s \<Longrightarrow> valid_pspace s proof (prove)
goal (4 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. \<not> is_final_cap' capa s \<and> cap = NullCap \<and> replaceable_non_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q10\<rbrace>
 2. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. \<not> is_final_cap' capa s \<and> cap = NullCap \<and> replaceable_non_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q10\<rbrace>
 3. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. is_final_cap' capa s \<and> (\<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>p'. p' \<in> cte_refs capa (interrupt_irq_node s) \<and> p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> p' \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs capa \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa) \<and> (is_master_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (is_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap capa \<longrightarrow> tcb_cap_valid capa p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa) \<and> replaceable_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q'10\<rbrace>
 4. \<And>rv s. valid_pspace s \<or> ?Q10 rv s \<or> ?Q'10 rv s \<Longrightarrow> valid_pspace s proof (prove)
goal (4 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s \<and> replaceable_non_final_arch_cap s p NullCap cap) p s \<and> tcb_cap_valid NullCap p s\<rbrace> set_cap NullCap p \<lbrace>?Q10\<rbrace>
 2. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. \<not> is_final_cap' capa s \<and> cap = NullCap \<and> replaceable_non_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q10\<rbrace>
 3. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. is_final_cap' capa s \<and> (\<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>p'. p' \<in> cte_refs capa (interrupt_irq_node s) \<and> p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> p' \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs capa \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa) \<and> (is_master_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (is_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap capa \<longrightarrow> tcb_cap_valid capa p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa) \<and> replaceable_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q'10\<rbrace>
 4. \<And>rv s. valid_pspace s \<or> ?Q10 rv s \<or> ?Q'10 rv s \<Longrightarrow> valid_pspace s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>cap = NullCap; valid_pspace s \<and> cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s \<and> replaceable_non_final_arch_cap s p NullCap cap) p s \<and> tcb_cap_valid NullCap p s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s) p s \<and> tcb_cap_valid NullCap p s
 2. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. \<not> is_final_cap' capa s \<and> cap = NullCap \<and> replaceable_non_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_pspace\<rbrace>
 3. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. is_final_cap' capa s \<and> (\<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>p'. p' \<in> cte_refs capa (interrupt_irq_node s) \<and> p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> p' \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs capa \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa) \<and> (is_master_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (is_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap capa \<longrightarrow> tcb_cap_valid capa p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa) \<and> replaceable_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q'10\<rbrace>
 4. \<And>rv s. valid_pspace s \<or> valid_pspace s \<or> ?Q'10 rv s \<Longrightarrow> valid_pspace s proof (prove)
goal (3 subgoals):
 1. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. \<not> is_final_cap' capa s \<and> cap = NullCap \<and> replaceable_non_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_pspace\<rbrace>
 2. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. is_final_cap' capa s \<and> (\<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>p'. p' \<in> cte_refs capa (interrupt_irq_node s) \<and> p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> p' \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs capa \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa) \<and> (is_master_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (is_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap capa \<longrightarrow> tcb_cap_valid capa p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa) \<and> replaceable_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q'10\<rbrace>
 3. \<And>rv s. valid_pspace s \<or> valid_pspace s \<or> ?Q'10 rv s \<Longrightarrow> valid_pspace s proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. is_final_cap' capa s \<and> (\<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>p'. p' \<in> cte_refs capa (interrupt_irq_node s) \<and> p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> p' \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs capa \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa) \<and> (is_master_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (is_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap capa \<longrightarrow> tcb_cap_valid capa p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa) \<and> replaceable_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s\<rbrace> set_cap cap p \<lbrace>?Q'10\<rbrace>
 2. \<And>rv s. valid_pspace s \<or> valid_pspace s \<or> ?Q'10 rv s \<Longrightarrow> valid_pspace s proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_pspace s \<and> cte_wp_at (\<lambda>capa. is_final_cap' capa s \<and> (\<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>p'. p' \<in> cte_refs capa (interrupt_irq_node s) \<and> p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> p' \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs capa \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa) \<and> (is_master_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (is_reply_cap capa \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap capa \<longrightarrow> tcb_cap_valid capa p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa) \<and> replaceable_final_arch_cap s p cap capa) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s \<Longrightarrow> cte_wp_at (\<lambda>cap'. (\<forall>p'\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p' s) \<and> (\<forall>r\<in>ex_zombie_refs (cap, cap'). \<forall>p'. p \<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)) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s \<and> valid_pspace s
 2. \<And>rv s. valid_pspace s \<or> valid_pspace s \<or> valid_pspace s \<Longrightarrow> valid_pspace s proof (prove)
goal (2 subgoals):
 1. \<And>s capa r a b capaa. \<lbrakk>valid_pspace s; s \<turnstile> cap; tcb_cap_valid cap p s; fst (get_cap p s) = {(capa, s)}; is_final_cap' capa s; \<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s; \<forall>a b. ((a, b) \<in> cte_refs capa (interrupt_irq_node s) \<and> (a, b) \<notin> cte_refs cap (interrupt_irq_node s) \<longrightarrow> ((a, b) \<noteq> p \<longrightarrow> fst (get_cap (a, b) s) = {(NullCap, s)}) \<and> ((a, b) = p \<longrightarrow> cap = NullCap)) \<and> ((a, b) \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> ((a, b) \<noteq> p \<longrightarrow> fst (get_cap (a, b) s) = {(NullCap, s)}) \<and> ((a, b) = p \<longrightarrow> cap = NullCap)); gen_obj_refs cap \<subseteq> gen_obj_refs capa; cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa; is_master_reply_cap capa \<longrightarrow> cap = NullCap; is_reply_cap capa \<longrightarrow> cap = NullCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; cap \<noteq> IRQControlCap; cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa; replaceable_final_arch_cap s p cap capa; r \<in> ex_zombie_refs (cap, capa); p \<noteq> (a, b); fst (get_cap (a, b) s) = {(capaa, s)}; r \<in> obj_refs capaa\<rbrakk> \<Longrightarrow> \<not> is_zombie capaa \<and> \<not> is_zombie cap
 2. \<And>rv s. valid_pspace s \<or> valid_pspace s \<or> valid_pspace s \<Longrightarrow> valid_pspace s proof (prove)
goal (4 subgoals):
 1. \<And>s capa r a b capaa. \<lbrakk>p \<noteq> (a, b); fst (get_cap (a, b) s) = {(capaa, s)}; r \<in> obj_refs capaa; valid_pspace s; s \<turnstile> cap; tcb_cap_valid cap p s; fst (get_cap p s) = {(capa, s)}; is_final_cap' capa s; \<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s; \<forall>a b. ((a, b) \<in> cte_refs capa (interrupt_irq_node s) \<and> (a, b) \<notin> cte_refs cap (interrupt_irq_node s) \<longrightarrow> ((a, b) \<noteq> p \<longrightarrow> fst (get_cap (a, b) s) = {(NullCap, s)}) \<and> ((a, b) = p \<longrightarrow> cap = NullCap)) \<and> ((a, b) \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> ((a, b) \<noteq> p \<longrightarrow> fst (get_cap (a, b) s) = {(NullCap, s)}) \<and> ((a, b) = p \<longrightarrow> cap = NullCap)); gen_obj_refs cap \<subseteq> gen_obj_refs capa; cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa; is_master_reply_cap capa \<longrightarrow> cap = NullCap; is_reply_cap capa \<longrightarrow> cap = NullCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; cap \<noteq> IRQControlCap; cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa; replaceable_final_arch_cap s p cap capa; is_zombie cap; is_zombie capa; r \<in> obj_refs cap; r \<notin> obj_refs capa\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa r a b capaa. \<lbrakk>p \<noteq> (a, b); fst (get_cap (a, b) s) = {(capaa, s)}; r \<in> obj_refs capaa; valid_pspace s; s \<turnstile> cap; tcb_cap_valid cap p s; fst (get_cap p s) = {(capa, s)}; is_final_cap' capa s; \<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s; \<forall>a b. ((a, b) \<in> cte_refs capa (interrupt_irq_node s) \<and> (a, b) \<notin> cte_refs cap (interrupt_irq_node s) \<longrightarrow> ((a, b) \<noteq> p \<longrightarrow> fst (get_cap (a, b) s) = {(NullCap, s)}) \<and> ((a, b) = p \<longrightarrow> cap = NullCap)) \<and> ((a, b) \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> ((a, b) \<noteq> p \<longrightarrow> fst (get_cap (a, b) s) = {(NullCap, s)}) \<and> ((a, b) = p \<longrightarrow> cap = NullCap)); gen_obj_refs cap \<subseteq> gen_obj_refs capa; cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa; is_master_reply_cap capa \<longrightarrow> cap = NullCap; is_reply_cap capa \<longrightarrow> cap = NullCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; cap \<noteq> IRQControlCap; cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa; replaceable_final_arch_cap s p cap capa; is_zombie cap; \<not> is_zombie capa; r \<in> obj_refs cap\<rbrakk> \<Longrightarrow> False
 3. \<And>s capa r a b capaa. \<lbrakk>p \<noteq> (a, b); fst (get_cap (a, b) s) = {(capaa, s)}; r \<in> obj_refs capaa; valid_pspace s; s \<turnstile> cap; tcb_cap_valid cap p s; fst (get_cap p s) = {(capa, s)}; is_final_cap' capa s; \<forall>p\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p s; \<forall>a b. ((a, b) \<in> cte_refs capa (interrupt_irq_node s) \<and> (a, b) \<notin> cte_refs cap (interrupt_irq_node s) \<longrightarrow> ((a, b) \<noteq> p \<longrightarrow> fst (get_cap (a, b) s) = {(NullCap, s)}) \<and> ((a, b) = p \<longrightarrow> cap = NullCap)) \<and> ((a, b) \<in> cte_refs capa (interrupt_irq_node s) \<and> (\<exists>cp. appropriate_cte_cap cp capa \<and> \<not> appropriate_cte_cap cp cap) \<longrightarrow> ((a, b) \<noteq> p \<longrightarrow> fst (get_cap (a, b) s) = {(NullCap, s)}) \<and> ((a, b) = p \<longrightarrow> cap = NullCap)); gen_obj_refs cap \<subseteq> gen_obj_refs capa; cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range capa; is_master_reply_cap capa \<longrightarrow> cap = NullCap; is_reply_cap capa \<longrightarrow> cap = NullCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; cap \<noteq> IRQControlCap; cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class capa \<and> cap_is_device cap = cap_is_device capa; replaceable_final_arch_cap s p cap capa; \<not> is_zombie cap; r \<in> obj_refs cap; r \<notin> obj_refs capa; is_zombie capaa\<rbrakk> \<Longrightarrow> False
 4. \<And>rv s. valid_pspace s \<or> valid_pspace s \<or> valid_pspace s \<Longrightarrow> valid_pspace s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. valid_pspace s \<or> valid_pspace s \<or> valid_pspace s \<Longrightarrow> valid_pspace s proof (prove)
goal:
No subgoals!