theory ArchCSpace_AI

lemma set_free_index_invs [CSpace_AI_assms]:
  "\<lbrace>\<lambda>s. (free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2^cap_bits cap) \<and>
        invs s \<and> cte_wp_at ((=) cap ) cref s\<rbrace>
   set_cap (free_index_update (\<lambda>_. idx) cap) cref
   \<lbrace>\<lambda>rv s'. invs s'\<rbrace>" apply (rule hoare_grab_asm)+ apply (simp add:invs_def valid_state_def) apply (rule hoare_pre) apply (wp set_free_index_valid_pspace[where cap = cap] set_free_index_valid_mdb
    set_cap_idle update_cap_ifunsafe) apply (simp add:valid_irq_node_def) apply wps apply (wp hoare_vcg_all_lift set_cap_irq_handlers set_cap_valid_arch_caps
    set_cap_irq_handlers cap_table_at_lift_valid set_cap_typ_at
    set_cap_cap_refs_respects_device_region_spec[where ptr = cref]) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (rule conjI,simp add:valid_pspace_def) apply (rule conjI,clarsimp simp:is_cap_simps) apply (rule conjI,rule ext,clarsimp simp: is_cap_simps) apply (clarsimp simp:is_cap_simps appropriate_cte_cap_def) apply (intro conjI) apply (clarsimp split:cap.splits) apply (drule(1) if_unsafe_then_capD[OF caps_of_state_cteD]) apply clarsimp apply (simp add:ex_cte_cap_wp_to_def appropriate_cte_cap_def) apply (clarsimp dest!:valid_global_refsD2 simp:cap_range_def) apply (simp add:valid_irq_node_def) apply clarsimp apply (clarsimp simp:valid_irq_node_def) apply (clarsimp simp:no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state vs_cap_ref_def) apply (case_tac capa) apply (simp_all add:table_cap_ref_def) apply (rename_tac arch_cap) apply (case_tac arch_cap) apply simp_all apply (clarsimp simp:cap_refs_in_kernel_window_def
              valid_refs_def simp del:split_paired_All) apply (drule_tac x = cref in spec) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (drule_tac x = ref in orthD2[rotated]) apply (simp add:cap_range_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap) \<and> invs s \<and> cte_wp_at ((=) cap) cref s\<rbrace> set_cap (free_index_update (\<lambda>_. idx) cap) cref \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> cte_wp_at ((=) cap) cref s\<rbrace> set_cap (free_index_update (\<lambda>_. idx) cap) cref \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap \<Longrightarrow> \<lbrace>\<lambda>s. valid_pspace s \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps 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 s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> cte_wp_at ((=) cap) cref s\<rbrace> set_cap (free_index_update (\<lambda>_. idx) cap) cref \<lbrace>\<lambda>rv s'. valid_pspace s' \<and> valid_mdb s' \<and> valid_ioc s' \<and> valid_idle s' \<and> only_idle s' \<and> if_unsafe_then_cap s' \<and> valid_reply_caps s' \<and> valid_reply_masters s' \<and> valid_global_refs s' \<and> valid_arch_state s' \<and> valid_irq_node s' \<and> valid_irq_handlers s' \<and> valid_irq_states s' \<and> valid_machine_state s' \<and> valid_vspace_objs s' \<and> valid_arch_caps 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 s' \<and> pspace_respects_device_region s' \<and> cap_refs_respects_device_region s' \<and> cur_tcb s'\<rbrace> proof (prove)
goal (2 subgoals):
 1. free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap \<Longrightarrow> \<lbrace>?Q2\<rbrace> set_cap (free_index_update (\<lambda>_. idx) cap) cref \<lbrace>\<lambda>rv s'. valid_pspace s' \<and> valid_mdb s' \<and> valid_ioc s' \<and> valid_idle s' \<and> only_idle s' \<and> if_unsafe_then_cap s' \<and> valid_reply_caps s' \<and> valid_reply_masters s' \<and> valid_global_refs s' \<and> valid_arch_state s' \<and> valid_irq_node s' \<and> valid_irq_handlers s' \<and> valid_irq_states s' \<and> valid_machine_state s' \<and> valid_vspace_objs s' \<and> valid_arch_caps 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 s' \<and> pspace_respects_device_region s' \<and> cap_refs_respects_device_region s' \<and> cur_tcb s'\<rbrace>
 2. \<And>s. \<lbrakk>free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap; valid_pspace s \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps 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 s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> cte_wp_at ((=) cap) cref s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap \<Longrightarrow> \<lbrace>?P'24\<rbrace> set_cap (free_index_update (\<lambda>_. idx) cap) cref \<lbrace>\<lambda>rv s. valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps 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 s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s\<rbrace>
 2. \<And>s. \<lbrakk>free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap; valid_pspace s \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps 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 s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> cte_wp_at ((=) cap) cref s\<rbrakk> \<Longrightarrow> (valid_pspace s \<and> cte_wp_at ((=) cap) cref s \<and> free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap) \<and> (valid_objs s \<and> valid_mdb s \<and> cte_wp_at ((=) cap) cref s \<and> free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap) \<and> (valid_ioc and (\<lambda>s. free_index_update (\<lambda>_. idx) cap = NullCap \<longrightarrow> \<not> is_original_cap s cref)) s \<and> valid_idle s \<and> only_idle s \<and> (cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs (free_index_update (\<lambda>_. idx) cap) \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp (free_index_update (\<lambda>_. idx) cap))) cref and if_unsafe_then_cap and (\<lambda>s. free_index_update (\<lambda>_. idx) cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (free_index_update (\<lambda>_. idx) cap)) cref s)) s \<and> (valid_reply_caps and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>t rights. free_index_update (\<lambda>_. idx) cap = ReplyCap t False rights \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (\<not> has_reply_cap t s \<or> cte_wp_at (is_reply_cap_to t) cref s))) s \<and> (valid_reply_masters and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>x. (\<exists>rights. free_index_update (\<lambda>_. idx) cap = ReplyCap x True rights) \<longrightarrow> fst cref = x \<and> snd cref = tcb_cnode_index 2)) s \<and> (valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range (free_index_update (\<lambda>_. idx) cap) = {})) s \<and> valid_arch_state s \<and> ?P'24 s proof (prove)
goal (2 subgoals):
 1. free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap \<Longrightarrow> \<lbrace>?P'24\<rbrace> set_cap (free_index_update (\<lambda>_. idx) cap) cref \<lbrace>\<lambda>rv s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s) \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps 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 s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s\<rbrace>
 2. \<And>s. \<lbrakk>free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap; valid_pspace s \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps 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 s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> cte_wp_at ((=) cap) cref s\<rbrakk> \<Longrightarrow> (valid_pspace s \<and> cte_wp_at ((=) cap) cref s \<and> free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap) \<and> (valid_objs s \<and> valid_mdb s \<and> cte_wp_at ((=) cap) cref s \<and> free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap) \<and> (valid_ioc and (\<lambda>s. free_index_update (\<lambda>_. idx) cap = NullCap \<longrightarrow> \<not> is_original_cap s cref)) s \<and> valid_idle s \<and> only_idle s \<and> (cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs (free_index_update (\<lambda>_. idx) cap) \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp (free_index_update (\<lambda>_. idx) cap))) cref and if_unsafe_then_cap and (\<lambda>s. free_index_update (\<lambda>_. idx) cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (free_index_update (\<lambda>_. idx) cap)) cref s)) s \<and> (valid_reply_caps and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>t rights. free_index_update (\<lambda>_. idx) cap = ReplyCap t False rights \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (\<not> has_reply_cap t s \<or> cte_wp_at (is_reply_cap_to t) cref s))) s \<and> (valid_reply_masters and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>x. (\<exists>rights. free_index_update (\<lambda>_. idx) cap = ReplyCap x True rights) \<longrightarrow> fst cref = x \<and> snd cref = tcb_cnode_index 2)) s \<and> (valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range (free_index_update (\<lambda>_. idx) cap) = {})) s \<and> valid_arch_state s \<and> ?P'24 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap \<Longrightarrow> \<lbrace>?P27 prev_s\<rbrace> set_cap (free_index_update (\<lambda>_. idx) cap) cref \<lbrace>\<lambda>rv s'. inj (interrupt_irq_node prev_s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node prev_s irq) s') \<and> valid_irq_handlers s' \<and> valid_irq_states s' \<and> valid_machine_state s' \<and> valid_vspace_objs s' \<and> valid_arch_caps 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 s' \<and> pspace_respects_device_region s' \<and> cap_refs_respects_device_region s' \<and> cur_tcb s'\<rbrace>
 2. \<And>s. \<lbrakk>free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap; valid_pspace s \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps 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 s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> cte_wp_at ((=) cap) cref s\<rbrakk> \<Longrightarrow> (valid_pspace s \<and> cte_wp_at ((=) cap) cref s \<and> free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap) \<and> (valid_objs s \<and> valid_mdb s \<and> cte_wp_at ((=) cap) cref s \<and> free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap) \<and> (valid_ioc and (\<lambda>s. free_index_update (\<lambda>_. idx) cap = NullCap \<longrightarrow> \<not> is_original_cap s cref)) s \<and> valid_idle s \<and> only_idle s \<and> (cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs (free_index_update (\<lambda>_. idx) cap) \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp (free_index_update (\<lambda>_. idx) cap))) cref and if_unsafe_then_cap and (\<lambda>s. free_index_update (\<lambda>_. idx) cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (free_index_update (\<lambda>_. idx) cap)) cref s)) s \<and> (valid_reply_caps and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>t rights. free_index_update (\<lambda>_. idx) cap = ReplyCap t False rights \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (\<not> has_reply_cap t s \<or> cte_wp_at (is_reply_cap_to t) cref s))) s \<and> (valid_reply_masters and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>x. (\<exists>rights. free_index_update (\<lambda>_. idx) cap = ReplyCap x True rights) \<longrightarrow> fst cref = x \<and> snd cref = tcb_cnode_index 2)) s \<and> (valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range (free_index_update (\<lambda>_. idx) cap) = {})) s \<and> valid_arch_state s \<and> ?P27 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap; valid_pspace s \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps 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 s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> cte_wp_at ((=) cap) cref s\<rbrakk> \<Longrightarrow> (valid_pspace s \<and> cte_wp_at ((=) cap) cref s \<and> free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap) \<and> (valid_objs s \<and> valid_mdb s \<and> cte_wp_at ((=) cap) cref s \<and> free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap) \<and> (valid_ioc and (\<lambda>s. free_index_update (\<lambda>_. idx) cap = NullCap \<longrightarrow> \<not> is_original_cap s cref)) s \<and> valid_idle s \<and> only_idle s \<and> (cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs (free_index_update (\<lambda>_. idx) cap) \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp (free_index_update (\<lambda>_. idx) cap))) cref and if_unsafe_then_cap and (\<lambda>s. free_index_update (\<lambda>_. idx) cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (free_index_update (\<lambda>_. idx) cap)) cref s)) s \<and> (valid_reply_caps and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>t rights. free_index_update (\<lambda>_. idx) cap = ReplyCap t False rights \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (\<not> has_reply_cap t s \<or> cte_wp_at (is_reply_cap_to t) cref s))) s \<and> (valid_reply_masters and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>x. (\<exists>rights. free_index_update (\<lambda>_. idx) cap = ReplyCap x True rights) \<longrightarrow> fst cref = x \<and> snd cref = tcb_cnode_index 2)) s \<and> (valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range (free_index_update (\<lambda>_. idx) cap) = {})) s \<and> valid_arch_state s \<and> inj (interrupt_irq_node s) \<and> (\<forall>x. cap_table_at 0 (interrupt_irq_node s x) s) \<and> (valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs (free_index_update (\<lambda>_. idx) cap) - cap_irqs cap'. irq_issued irq s) cref s) \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> (valid_arch_caps s \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') cref s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref (free_index_update (\<lambda>_. idx) cap) = Some vref \<and> obj_refs (free_index_update (\<lambda>_. idx) cap) = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (free_index_update (\<lambda>_. idx) cap) {cref} s \<and> (is_pt_cap (free_index_update (\<lambda>_. idx) cap) \<or> is_pd_cap (free_index_update (\<lambda>_. idx) cap) \<longrightarrow> cap_asid (free_index_update (\<lambda>_. idx) cap) = None \<longrightarrow> (\<forall>r\<in>obj_refs (free_index_update (\<lambda>_. idx) cap). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap (free_index_update (\<lambda>_. idx) cap) \<or> is_pd_cap (free_index_update (\<lambda>_. idx) cap) \<longrightarrow> (\<forall>oldcap. caps_of_state s cref = Some oldcap \<longrightarrow> is_pt_cap (free_index_update (\<lambda>_. idx) cap) \<and> is_pt_cap oldcap \<or> is_pd_cap (free_index_update (\<lambda>_. idx) cap) \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid (free_index_update (\<lambda>_. idx) cap) = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs (free_index_update (\<lambda>_. idx) cap)) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs (free_index_update (\<lambda>_. idx) cap) \<and> (is_pd_cap (free_index_update (\<lambda>_. idx) cap) \<and> is_pd_cap cap' \<or> is_pt_cap (free_index_update (\<lambda>_. idx) cap) \<and> is_pt_cap cap') \<and> (cap_asid (free_index_update (\<lambda>_. idx) cap) = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = cref))) \<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 (\<lambda>s. \<forall>ref\<in>cap_range (free_index_update (\<lambda>_. idx) cap). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow)) s \<and> pspace_respects_device_region s \<and> (cap_refs_respects_device_region and cte_wp_at (\<lambda>c. cap_range (free_index_update (\<lambda>_. idx) cap) \<subseteq> cap_range c \<and> (cap_range (free_index_update (\<lambda>_. idx) cap) \<noteq> {} \<longrightarrow> cap_is_device (free_index_update (\<lambda>_. idx) cap) = cap_is_device c)) cref) s \<and> cur_tcb s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>free_index_of cap \<le> idx; valid_pspace s; is_untyped_cap cap; idx \<le> 2 ^ cap_bits cap; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some cap\<rbrakk> \<Longrightarrow> valid_objs s \<and> (free_index_update (\<lambda>_. idx) cap = NullCap \<longrightarrow> \<not> is_original_cap s cref) \<and> cte_refs cap = cte_refs (free_index_update (\<lambda>_. idx) cap) \<and> (\<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp (free_index_update (\<lambda>_. idx) cap)) \<and> (free_index_update (\<lambda>_. idx) cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (free_index_update (\<lambda>_. idx) cap)) cref s) \<and> (\<forall>t. (\<exists>rights. free_index_update (\<lambda>_. idx) cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (has_reply_cap t s \<longrightarrow> is_reply_cap_to t cap)) \<and> (\<forall>x. (\<exists>rights. free_index_update (\<lambda>_. idx) cap = ReplyCap x True rights) \<longrightarrow> fst cref = x \<and> snd cref = tcb_cnode_index 2) \<and> global_refs s \<inter> cap_range cap = {} \<and> inj (interrupt_irq_node s) \<and> (\<forall>x. cap_table_at 0 (interrupt_irq_node s x) s) \<and> (\<forall>irq\<in>cap_irqs (free_index_update (\<lambda>_. idx) cap) - cap_irqs cap. irq_issued irq s) \<and> no_cap_to_obj_with_diff_ref (free_index_update (\<lambda>_. idx) cap) {cref} 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> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device (free_index_update (\<lambda>_. idx) cap) = cap_is_device cap) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>free_index_of cap \<le> idx; valid_pspace s; is_untyped_cap cap; idx \<le> 2 ^ cap_bits cap; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some cap\<rbrakk> \<Longrightarrow> (free_index_update (\<lambda>_. idx) cap = NullCap \<longrightarrow> \<not> is_original_cap s cref) \<and> cte_refs cap = cte_refs (free_index_update (\<lambda>_. idx) cap) \<and> (\<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp (free_index_update (\<lambda>_. idx) cap)) \<and> (free_index_update (\<lambda>_. idx) cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (free_index_update (\<lambda>_. idx) cap)) cref s) \<and> (\<forall>t. (\<exists>rights. free_index_update (\<lambda>_. idx) cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (has_reply_cap t s \<longrightarrow> is_reply_cap_to t cap)) \<and> (\<forall>x. (\<exists>rights. free_index_update (\<lambda>_. idx) cap = ReplyCap x True rights) \<longrightarrow> fst cref = x \<and> snd cref = tcb_cnode_index 2) \<and> global_refs s \<inter> cap_range cap = {} \<and> inj (interrupt_irq_node s) \<and> (\<forall>x. cap_table_at 0 (interrupt_irq_node s x) s) \<and> (\<forall>irq\<in>cap_irqs (free_index_update (\<lambda>_. idx) cap) - cap_irqs cap. irq_issued irq s) \<and> no_cap_to_obj_with_diff_ref (free_index_update (\<lambda>_. idx) cap) {cref} 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> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device (free_index_update (\<lambda>_. idx) cap) = cap_is_device cap) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>free_index_of cap \<le> idx; valid_pspace s; is_untyped_cap cap; idx \<le> 2 ^ cap_bits cap; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some cap\<rbrakk> \<Longrightarrow> cte_refs cap = cte_refs (free_index_update (\<lambda>_. idx) cap) \<and> (\<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp (free_index_update (\<lambda>_. idx) cap)) \<and> (free_index_update (\<lambda>_. idx) cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (free_index_update (\<lambda>_. idx) cap)) cref s) \<and> (\<forall>t. (\<exists>rights. free_index_update (\<lambda>_. idx) cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (has_reply_cap t s \<longrightarrow> is_reply_cap_to t cap)) \<and> (\<forall>x. (\<exists>rights. free_index_update (\<lambda>_. idx) cap = ReplyCap x True rights) \<longrightarrow> fst cref = x \<and> snd cref = tcb_cnode_index 2) \<and> global_refs s \<inter> cap_range cap = {} \<and> inj (interrupt_irq_node s) \<and> (\<forall>x. cap_table_at 0 (interrupt_irq_node s x) s) \<and> (\<forall>irq\<in>cap_irqs (free_index_update (\<lambda>_. idx) cap) - cap_irqs cap. irq_issued irq s) \<and> no_cap_to_obj_with_diff_ref (free_index_update (\<lambda>_. idx) cap) {cref} 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> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device (free_index_update (\<lambda>_. idx) cap) = cap_is_device cap) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>free_index_of cap \<le> idx; valid_pspace s; is_untyped_cap cap; idx \<le> 2 ^ cap_bits cap; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some cap\<rbrakk> \<Longrightarrow> (\<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp (free_index_update (\<lambda>_. idx) cap)) \<and> (free_index_update (\<lambda>_. idx) cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (free_index_update (\<lambda>_. idx) cap)) cref s) \<and> (\<forall>t. (\<exists>rights. free_index_update (\<lambda>_. idx) cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (has_reply_cap t s \<longrightarrow> is_reply_cap_to t cap)) \<and> (\<forall>x. (\<exists>rights. free_index_update (\<lambda>_. idx) cap = ReplyCap x True rights) \<longrightarrow> fst cref = x \<and> snd cref = tcb_cnode_index 2) \<and> global_refs s \<inter> cap_range cap = {} \<and> inj (interrupt_irq_node s) \<and> (\<forall>x. cap_table_at 0 (interrupt_irq_node s x) s) \<and> (\<forall>irq\<in>cap_irqs (free_index_update (\<lambda>_. idx) cap) - cap_irqs cap. irq_issued irq s) \<and> no_cap_to_obj_with_diff_ref (free_index_update (\<lambda>_. idx) cap) {cref} 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> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device (free_index_update (\<lambda>_. idx) cap) = cap_is_device cap) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> (\<forall>cp. (case cp of NullCap \<Rightarrow> True | NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs (UntypedCap dev r bits f) = {}) = (case cp of NullCap \<Rightarrow> True | NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs (free_index_update (\<lambda>_. idx) (UntypedCap dev r bits f)) = {})) \<and> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev r bits idx)) cref s \<and> global_refs s \<inter> cap_range (UntypedCap dev r bits f) = {} \<and> inj (interrupt_irq_node s) \<and> (\<forall>x. cap_table_at 0 (interrupt_irq_node s x) s) \<and> no_cap_to_obj_with_diff_ref (UntypedCap dev r bits idx) {cref} s \<and> (\<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) proof (prove)
goal (7 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>cp. (case cp of NullCap \<Rightarrow> True | NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs (UntypedCap dev r bits f) = {}) = (case cp of NullCap \<Rightarrow> True | NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs (free_index_update (\<lambda>_. idx) (UntypedCap dev r bits f)) = {})
 2. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev r bits idx)) cref s
 3. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (UntypedCap dev r bits f) = {}
 4. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node s)
 5. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>x. cap_table_at 0 (interrupt_irq_node s x) s
 6. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev r bits idx) {cref} s
 7. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (6 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev r bits idx)) cref s
 2. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (UntypedCap dev r bits f) = {}
 3. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node s)
 4. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>x. cap_table_at 0 (interrupt_irq_node s x) s
 5. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev r bits idx) {cref} s
 6. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (7 subgoals):
 1. \<And>s dev r bits f capa. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cap = UntypedCap dev r bits f; UntypedCap dev r bits f = capa\<rbrakk> \<Longrightarrow> capa \<noteq> NullCap
 2. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cap = UntypedCap dev r bits f; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. UntypedCap dev r bits f = cap' \<and> appropriate_cte_cap cap' cap) cref s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev r bits idx)) cref s
 3. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (UntypedCap dev r bits f) = {}
 4. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node s)
 5. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>x. cap_table_at 0 (interrupt_irq_node s x) s
 6. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev r bits idx) {cref} s
 7. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (6 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cap = UntypedCap dev r bits f; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. UntypedCap dev r bits f = cap' \<and> appropriate_cte_cap cap' cap) cref s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev r bits idx)) cref s
 2. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (UntypedCap dev r bits f) = {}
 3. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node s)
 4. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>x. cap_table_at 0 (interrupt_irq_node s x) s
 5. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev r bits idx) {cref} s
 6. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (5 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (UntypedCap dev r bits f) = {}
 2. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node s)
 3. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>x. cap_table_at 0 (interrupt_irq_node s x) s
 4. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev r bits idx) {cref} s
 5. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (4 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node s)
 2. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>x. cap_table_at 0 (interrupt_irq_node s x) s
 3. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev r bits idx) {cref} s
 4. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (3 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>x. cap_table_at 0 (interrupt_irq_node s x) s
 2. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev r bits idx) {cref} s
 3. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (3 subgoals):
 1. \<And>s dev r bits f x. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> cap_table_at 0 (interrupt_irq_node s x) s
 2. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev r bits idx) {cref} s
 3. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev r bits idx) {cref} s
 2. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f a b capa. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; obj_refs capa = {}; caps_of_state s (a, b) = Some capa\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref (UntypedCap dev r bits idx)
 2. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (13 subgoals):
 1. \<And>s dev r bits f a b capa. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; obj_refs capa = {}; caps_of_state s (a, b) = Some capa; capa = NullCap\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref (UntypedCap dev r bits idx)
 2. \<And>s dev r bits f a b capa x21 x22 x23 x24. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; obj_refs capa = {}; caps_of_state s (a, b) = Some capa; capa = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref (UntypedCap dev r bits idx)
 3. \<And>s dev r bits f a b capa x31 x32 x33. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; obj_refs capa = {}; caps_of_state s (a, b) = Some capa; capa = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref (UntypedCap dev r bits idx)
 4. \<And>s dev r bits f a b capa x41 x42 x43. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; obj_refs capa = {}; caps_of_state s (a, b) = Some capa; capa = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref (UntypedCap dev r bits idx)
 5. \<And>s dev r bits f a b capa x51 x52 x53. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; obj_refs capa = {}; caps_of_state s (a, b) = Some capa; capa = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref (UntypedCap dev r bits idx)
 6. \<And>s dev r bits f a b capa x61 x62 x63. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; obj_refs capa = {}; caps_of_state s (a, b) = Some capa; capa = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref (UntypedCap dev r bits idx)
 7. \<And>s dev r bits f a b capa x7. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; obj_refs capa = {}; caps_of_state s (a, b) = Some capa; capa = ThreadCap x7\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref (UntypedCap dev r bits idx)
 8. \<And>s dev r bits f a b capa. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; obj_refs capa = {}; caps_of_state s (a, b) = Some capa; capa = DomainCap\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref (UntypedCap dev r bits idx)
 9. \<And>s dev r bits f a b capa. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; obj_refs capa = {}; caps_of_state s (a, b) = Some capa; capa = IRQControlCap\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref (UntypedCap dev r bits idx)
 10. \<And>s dev r bits f a b capa x10. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; obj_refs capa = {}; caps_of_state s (a, b) = Some capa; capa = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref (UntypedCap dev r bits idx)
A total of 13 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f a b capa x12. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; aobj_ref x12 = None; caps_of_state s (a, b) = Some (ArchObjectCap x12); capa = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (case x12 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = None
 2. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f a b capa arch_cap. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; aobj_ref arch_cap = None; caps_of_state s (a, b) = Some (ArchObjectCap arch_cap); capa = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (case arch_cap of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = None
 2. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (6 subgoals):
 1. \<And>s dev r bits f a b capa arch_cap x11 x12. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; aobj_ref arch_cap = None; caps_of_state s (a, b) = Some (ArchObjectCap arch_cap); capa = ArchObjectCap arch_cap; arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> (case arch_cap of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = None
 2. \<And>s dev r bits f a b capa arch_cap. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; aobj_ref arch_cap = None; caps_of_state s (a, b) = Some (ArchObjectCap arch_cap); capa = ArchObjectCap arch_cap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> (case arch_cap of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = None
 3. \<And>s dev r bits f a b capa arch_cap x31 x32 x33 x34 x35. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; aobj_ref arch_cap = None; caps_of_state s (a, b) = Some (ArchObjectCap arch_cap); capa = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> (case arch_cap of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = None
 4. \<And>s dev r bits f a b capa arch_cap x41 x42. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; aobj_ref arch_cap = None; caps_of_state s (a, b) = Some (ArchObjectCap arch_cap); capa = ArchObjectCap arch_cap; arch_cap = PageTableCap x41 x42\<rbrakk> \<Longrightarrow> (case arch_cap of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = None
 5. \<And>s dev r bits f a b capa arch_cap x51 x52. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; (a, b) \<noteq> cref; aobj_ref arch_cap = None; caps_of_state s (a, b) = Some (ArchObjectCap arch_cap); capa = ArchObjectCap arch_cap; arch_cap = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> (case arch_cap of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = None
 6. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range (UntypedCap dev r bits f). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f ref. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; \<forall>cref. \<not> cte_wp_at (\<lambda>c. {x. arm_kernel_vspace (arch_state s) x \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range c \<noteq> {}) cref s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; ref \<in> cap_range (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f ref. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; ref \<in> cap_range (UntypedCap dev r bits f); \<not> cte_wp_at (\<lambda>c. {x. arm_kernel_vspace (arch_state s) x \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range c \<noteq> {}) cref s\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f ref. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; ref \<in> cap_range (UntypedCap dev r bits f); {x. arm_kernel_vspace (arch_state s) x \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range (UntypedCap dev r bits f) = {}\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f ref. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; {x. arm_kernel_vspace (arch_state s) x \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range (UntypedCap dev r bits f) = {}\<rbrakk> \<Longrightarrow> ?S179 s dev r bits f ref \<inter> cap_range (UntypedCap dev r bits f) = {}
 2. \<And>s dev r bits f ref. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; {x. arm_kernel_vspace (arch_state s) x \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range (UntypedCap dev r bits f) = {}; ref \<notin> ?S179 s dev r bits f ref\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f ref. \<lbrakk>free_index_of (UntypedCap dev r bits f) \<le> idx; valid_pspace s; idx \<le> 2 ^ bits; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; {x. arm_kernel_vspace (arch_state s) x \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range (UntypedCap dev r bits f) = {}; ref \<notin> {x. arm_kernel_vspace (arch_state s) x \<noteq> ArmVSpaceKernelWindow}\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal:
No subgoals!