theory CSpace_AI

lemma cap_insert_invs[wp]:
  "\<And>dest cap src.
    \<lbrace>invs and cte_wp_at (\<lambda>c. c=Structures_A.NullCap) dest
          and valid_cap cap and tcb_cap_valid cap dest
          and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest
          and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>p'. dest \<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))
          and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s)
          and (\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq \<in> cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s)
          and (\<lambda>s. \<forall>t R. cap = cap.ReplyCap t False R \<longrightarrow>
                   st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s)
          and K (\<not> is_master_reply_cap cap)\<rbrace>
      cap_insert cap src dest
    \<lbrace>\<lambda>rv. invs :: 'state_ext state \<Rightarrow> bool\<rbrace>" apply (simp add: invs_def valid_state_def) apply (rule hoare_pre) apply (wp cap_insert_valid_pspace cap_insert_ifunsafe cap_insert_idle
             valid_irq_node_typ cap_insert_valid_arch_caps cap_insert_derived_ioports) apply (auto simp: cte_wp_at_caps_of_state is_derived_cap_is_device
                        is_derived_cap_range valid_pspace_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>dest cap src. \<lbrace>invs and cte_wp_at (\<lambda>c. c = NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>p'. dest \<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) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and (\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s) and (\<lambda>s. \<forall>t R. cap = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) and K (\<not> is_master_reply_cap cap)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>dest cap src. \<lbrace>valid_pspace and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and cte_wp_at (\<lambda>c. c = NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and (\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s) and (\<lambda>s. \<forall>t. (\<exists>R. cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) and (\<lambda>y. \<not> is_master_reply_cap cap)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. valid_pspace and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>dest cap src. \<lbrace>?Q6 dest cap src\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. valid_pspace and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace>
 2. \<And>dest cap src s. (valid_pspace and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and cte_wp_at (\<lambda>c. c = NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and (\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s) and (\<lambda>s. \<forall>t. (\<exists>R. cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) and (\<lambda>y. \<not> is_master_reply_cap cap)) s \<Longrightarrow> ?Q6 dest cap src s proof (prove)
goal (1 subgoal):
 1. \<And>dest cap src s. (valid_pspace and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and cte_wp_at (\<lambda>c. c = NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. dest \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and (\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s) and (\<lambda>s. \<forall>t. (\<exists>R. cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) and (\<lambda>y. \<not> is_master_reply_cap cap)) s \<Longrightarrow> (valid_pspace and cte_wp_at ((=) NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>p'. dest \<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)) s \<and> (valid_mdb and valid_cap cap and valid_objs and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and K (src \<noteq> dest)) s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> (if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest) s \<and> (valid_reply_caps and cte_wp_at (\<lambda>_. True) dest and (\<lambda>s. \<forall>t R. cap = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s)) s \<and> (valid_reply_masters and cte_wp_at (\<lambda>_. True) dest and K (\<not> is_master_reply_cap cap)) s \<and> (valid_global_refs and cte_wp_at (\<lambda>scap. cap_range cap \<subseteq> cap_range scap) src) s \<and> valid_arch_state s \<and> valid_irq_node s \<and> (valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s) \<and> valid_irq_states s \<and> (valid_ioports and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s)) s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> (valid_arch_caps and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s)) s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> (cap_refs_in_kernel_window and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c) src) s \<and> pspace_respects_device_region s \<and> (cap_refs_respects_device_region and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device c)) src) s \<and> cur_tcb s proof (prove)
goal:
No subgoals!