theory ArchFinalise_AI

lemma (* dmo_replaceable_or_arch_update *) [Finalise_AI_asms,wp]:
  "\<lbrace>\<lambda>s. replaceable_or_arch_update s slot cap cap'\<rbrace>
    do_machine_op mo
  \<lbrace>\<lambda>r s. replaceable_or_arch_update s slot cap cap'\<rbrace>" unfolding replaceable_or_arch_update_def replaceable_def no_cap_to_obj_with_diff_ref_def
            replaceable_final_arch_cap_def replaceable_non_final_arch_cap_def apply (rule hoare_pre) apply (wps dmo_tcb_cap_valid_ARCH do_machine_op_reachable_pg_cap) apply (rule hoare_vcg_prop) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. replaceable_or_arch_update s slot cap cap'\<rbrace> do_machine_op mo \<lbrace>\<lambda>r s. replaceable_or_arch_update s slot cap cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if is_pg_cap cap then is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) else cap' = cap \<or> \<not> is_final_cap' cap' s \<and> cap = NullCap \<and> \<not> reachable_pg_cap cap' s \<or> is_final_cap' cap' s \<and> (\<forall>p\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<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> slot \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = slot \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs cap' \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range cap') \<and> (is_master_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (is_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap cap' \<longrightarrow> tcb_cap_valid cap' slot s \<longrightarrow> tcb_cap_valid cap slot 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 cap' \<and> cap_is_device cap = cap_is_device cap') \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> (\<forall>p\<in>UNIV - {slot}. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) p s) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap cap' \<or> is_pd_cap cap \<and> is_pd_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<longrightarrow> (\<forall>sl'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) sl' s \<longrightarrow> sl' = slot)) \<and> \<not> is_ap_cap cap\<rbrace> do_machine_op mo \<lbrace>\<lambda>r s. if is_pg_cap cap then is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) else cap' = cap \<or> \<not> is_final_cap' cap' s \<and> cap = NullCap \<and> \<not> reachable_pg_cap cap' s \<or> is_final_cap' cap' s \<and> (\<forall>p\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<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> slot \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = slot \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs cap' \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range cap') \<and> (is_master_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (is_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap cap' \<longrightarrow> tcb_cap_valid cap' slot s \<longrightarrow> tcb_cap_valid cap slot 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 cap' \<and> cap_is_device cap = cap_is_device cap') \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> (\<forall>p\<in>UNIV - {slot}. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) p s) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap cap' \<or> is_pd_cap cap \<and> is_pd_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<longrightarrow> (\<forall>sl'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) sl' s \<longrightarrow> sl' = slot)) \<and> \<not> is_ap_cap cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do_machine_op mo \<lbrace>\<lambda>r s. if is_pg_cap cap then is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) else cap' = cap \<or> \<not> is_final_cap' cap' s \<and> cap = NullCap \<and> \<not> reachable_pg_cap cap' s \<or> is_final_cap' cap' s \<and> (\<forall>p\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<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> slot \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = slot \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs cap' \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range cap') \<and> (is_master_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (is_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap cap' \<longrightarrow> tcb_cap_valid cap' slot s \<longrightarrow> tcb_cap_valid cap slot 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 cap' \<and> cap_is_device cap = cap_is_device cap') \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> (\<forall>p\<in>UNIV - {slot}. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) p s) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap cap' \<or> is_pd_cap cap \<and> is_pd_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<longrightarrow> (\<forall>sl'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) sl' s \<longrightarrow> sl' = slot)) \<and> \<not> is_ap_cap cap\<rbrace>
 2. \<And>s. if is_pg_cap cap then is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) else cap' = cap \<or> \<not> is_final_cap' cap' s \<and> cap = NullCap \<and> \<not> reachable_pg_cap cap' s \<or> is_final_cap' cap' s \<and> (\<forall>p\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<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> slot \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = slot \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs cap' \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range cap') \<and> (is_master_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (is_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap cap' \<longrightarrow> tcb_cap_valid cap' slot s \<longrightarrow> tcb_cap_valid cap slot 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 cap' \<and> cap_is_device cap = cap_is_device cap') \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> (\<forall>p\<in>UNIV - {slot}. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) p s) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap cap' \<or> is_pd_cap cap \<and> is_pd_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<longrightarrow> (\<forall>sl'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) sl' s \<longrightarrow> sl' = slot)) \<and> \<not> is_ap_cap cap \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> do_machine_op mo \<lbrace>\<lambda>rv s'. if is_pg_cap cap then is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages prev_s)) else cap' = cap \<or> \<not> is_final_cap' cap' prev_s \<and> cap = NullCap \<and> \<not> reachable_pg_cap cap' prev_s \<or> is_final_cap' cap' prev_s \<and> (\<forall>p\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p prev_s) \<and> (\<forall>p'. p' \<in> cte_refs cap' (interrupt_irq_node prev_s) \<and> (p' \<in> cte_refs cap (interrupt_irq_node prev_s) \<longrightarrow> (\<exists>cp. appropriate_cte_cap cp cap' \<and> \<not> appropriate_cte_cap cp cap)) \<longrightarrow> (p' \<noteq> slot \<longrightarrow> cte_wp_at ((=) NullCap) p' prev_s) \<and> (p' = slot \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs cap' \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range cap') \<and> (is_master_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (is_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap cap' \<longrightarrow> tcb_cap_valid cap' slot prev_s \<longrightarrow> tcb_cap_valid cap slot prev_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 cap' \<and> cap_is_device cap = cap_is_device cap') \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages prev_s)) \<and> (\<forall>p\<in>UNIV - {slot}. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) p prev_s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state prev_s)))) r prev_s)) \<and> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state prev_s)))) r prev_s)) \<and> (is_pt_cap cap \<longrightarrow> (is_pt_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<longrightarrow> (\<forall>sl'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) sl' prev_s \<longrightarrow> sl' = slot)) \<and> (is_pd_cap cap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<and> (is_pd_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<longrightarrow> (\<forall>sl'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) sl' prev_s \<longrightarrow> sl' = slot)) \<and> \<not> is_ap_cap cap\<rbrace>
 2. \<And>s. if is_pg_cap cap then is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) else cap' = cap \<or> \<not> is_final_cap' cap' s \<and> cap = NullCap \<and> \<not> reachable_pg_cap cap' s \<or> is_final_cap' cap' s \<and> (\<forall>p\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<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> slot \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = slot \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs cap' \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range cap') \<and> (is_master_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (is_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap cap' \<longrightarrow> tcb_cap_valid cap' slot s \<longrightarrow> tcb_cap_valid cap slot 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 cap' \<and> cap_is_device cap = cap_is_device cap') \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> (\<forall>p\<in>UNIV - {slot}. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) p s) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap cap' \<or> is_pd_cap cap \<and> is_pd_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<longrightarrow> (\<forall>sl'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) sl' s \<longrightarrow> sl' = slot)) \<and> \<not> is_ap_cap cap \<Longrightarrow> ?P3 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. if is_pg_cap cap then is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) else cap' = cap \<or> \<not> is_final_cap' cap' s \<and> cap = NullCap \<and> \<not> reachable_pg_cap cap' s \<or> is_final_cap' cap' s \<and> (\<forall>p\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<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> slot \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = slot \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs cap' \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range cap') \<and> (is_master_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (is_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap cap' \<longrightarrow> tcb_cap_valid cap' slot s \<longrightarrow> tcb_cap_valid cap slot 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 cap' \<and> cap_is_device cap = cap_is_device cap') \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> (\<forall>p\<in>UNIV - {slot}. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) p s) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap cap' \<or> is_pd_cap cap \<and> is_pd_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<longrightarrow> (\<forall>sl'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) sl' s \<longrightarrow> sl' = slot)) \<and> \<not> is_ap_cap cap \<Longrightarrow> if is_pg_cap cap then is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) else cap' = cap \<or> \<not> is_final_cap' cap' s \<and> cap = NullCap \<and> \<not> reachable_pg_cap cap' s \<or> is_final_cap' cap' s \<and> (\<forall>p\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>p'. p' \<in> cte_refs cap' (interrupt_irq_node s) \<and> (p' \<in> cte_refs cap (interrupt_irq_node s) \<longrightarrow> (\<exists>cp. appropriate_cte_cap cp cap' \<and> \<not> appropriate_cte_cap cp cap)) \<longrightarrow> (p' \<noteq> slot \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = slot \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs cap' \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range cap') \<and> (is_master_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (is_reply_cap cap' \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap cap' \<longrightarrow> tcb_cap_valid cap' slot s \<longrightarrow> tcb_cap_valid cap slot 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 cap' \<and> cap_is_device cap = cap_is_device cap') \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> (\<forall>p\<in>UNIV - {slot}. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) p s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<longrightarrow> (is_pt_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<longrightarrow> (\<forall>sl'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) sl' s \<longrightarrow> sl' = slot)) \<and> (is_pd_cap cap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<and> (is_pd_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<longrightarrow> (\<forall>sl'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) sl' s \<longrightarrow> sl' = slot)) \<and> \<not> is_ap_cap cap proof (prove)
goal:
No subgoals!