theory CSpaceInv_AI

lemma replace_cap_ifunsafe:
  "\<lbrace>\<lambda>s. cte_wp_at (replaceable s p cap) p s
       \<and> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s
       \<and> (cap \<noteq> cap.NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>" apply (simp only: replaceable_def cte_wp_at_disj conj_disj_distribR) apply (intro hoare_vcg_disj_lift[where Q=Q and Q'=Q for Q, simplified]) apply (wp set_cap_ifunsafe) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (cases "cap = cap.NullCap") apply simp apply (wp delete_duplicate_ifunsafe) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (simp add: cte_wp_at_caps_of_state) apply (wp set_cap_ifunsafe) apply (clarsimp simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (replaceable s p cap) p s \<and> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>capa. capa = cap) p s \<and> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s) \<or> 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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s) \<or> 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> (\<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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>capa. capa = cap) p s \<and> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>
 2. \<lbrace>\<lambda>s. 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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>
 3. \<lbrace>\<lambda>s. 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> (\<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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. cte_wp_at (\<lambda>capa. capa = cap) p s \<and> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s) \<Longrightarrow> cte_wp_at (\<lambda>cap'. \<forall>p'. p' \<in> cte_refs cap' (interrupt_irq_node s) \<and> (p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> (\<exists>cp. appropriate_cte_cap cp cap' \<and> \<not> appropriate_cte_cap cp cap)) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) p s \<and> if_unsafe_then_cap s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)
 2. \<lbrace>\<lambda>s. 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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>
 3. \<lbrace>\<lambda>s. 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> (\<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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. 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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>
 2. \<lbrace>\<lambda>s. 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> (\<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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (3 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>\<lambda>s. 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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>
 2. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>\<lambda>s. 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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>
 3. \<lbrace>\<lambda>s. 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> (\<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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (3 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s \<and> replaceable_non_final_arch_cap s p NullCap cap) p s \<and> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s\<rbrace> set_cap NullCap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>
 2. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>\<lambda>s. 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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>
 3. \<lbrace>\<lambda>s. 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> (\<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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>cap = NullCap; cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s \<and> replaceable_non_final_arch_cap s p NullCap cap) p s \<and> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s) p s \<and> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s
 2. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>\<lambda>s. 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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>
 3. \<lbrace>\<lambda>s. 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> (\<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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>\<lambda>s. 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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>
 2. \<lbrace>\<lambda>s. 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> (\<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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 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> (\<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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. 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> (\<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> if_unsafe_then_cap s \<and> valid_objs s \<and> zombies_final s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s) \<Longrightarrow> cte_wp_at (\<lambda>cap'. \<forall>p'. p' \<in> cte_refs cap' (interrupt_irq_node s) \<and> (p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> (\<exists>cp. appropriate_cte_cap cp cap' \<and> \<not> appropriate_cte_cap cp cap)) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) p s \<and> if_unsafe_then_cap s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s) proof (prove)
goal:
No subgoals!