theory Untyped_AI

lemma set_untyped_cap_invs_simple:
  "\<lbrace>\<lambda>s. descendants_range_in {ptr .. ptr+2^sz - 1} cref s
  \<and> pspace_no_overlap_range_cover ptr sz s \<and> invs s
  \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz
      \<and> cap_is_device c = dev\<and> obj_ref_of c = ptr) cref s \<and> idx \<le> 2^ sz\<rbrace>
  set_cap (UntypedCap dev ptr sz idx) cref
 \<lbrace>\<lambda>rv s. invs s\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp:cte_wp_at_caps_of_state invs_def valid_state_def) apply (rule hoare_pre) apply (wp set_free_index_valid_pspace_simple set_cap_valid_mdb_simple
     set_cap_idle update_cap_ifunsafe set_cap_valid_arch_caps_simple) apply (simp add:valid_irq_node_def) apply wps apply (wp hoare_vcg_all_lift set_cap_irq_handlers
     set_cap_irq_handlers cap_table_at_lift_valid set_cap_ioports'
     set_cap_typ_at set_cap_valid_arch_caps_simple set_cap_kernel_window_simple
     set_cap_cap_refs_respects_device_region) apply (clarsimp simp del: split_paired_Ex) apply (strengthen exI[where x=cref]) apply (clarsimp simp:cte_wp_at_caps_of_state is_cap_simps valid_pspace_def) apply (intro conjI; clarsimp?) apply (clarsimp simp: fun_eq_iff) apply (clarsimp split:cap.splits simp:is_cap_simps appropriate_cte_cap_def) apply (drule(1) if_unsafe_then_capD[OF caps_of_state_cteD]) apply clarsimp apply (clarsimp simp: is_cap_simps ex_cte_cap_wp_to_def appropriate_cte_cap_def
                            cte_wp_at_caps_of_state) apply (clarsimp dest!:valid_global_refsD2 simp:cap_range_def) apply (simp add:valid_irq_node_def) apply (clarsimp simp:valid_irq_node_def) apply (clarsimp intro!: safe_ioport_insert_triv simp: is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> cap_is_device c = dev \<and> obj_ref_of c = ptr) cref s \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> cap_is_device c = dev \<and> obj_ref_of c = ptr) cref s \<and> idx \<le> 2 ^ sz \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref s; pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s; valid_pspace s; 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_ioports 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; idx \<le> 2 ^ cap_bits cap; caps_of_state s cref = Some cap; is_untyped_cap cap; sz = cap_bits cap; dev = cap_is_device cap; ptr = obj_ref_of cap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) 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_ioports 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. \<And>s cap. \<lbrakk>descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref s; pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s; valid_pspace s; 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_ioports 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; idx \<le> 2 ^ cap_bits cap; caps_of_state s cref = Some cap; is_untyped_cap cap; sz = cap_bits cap; dev = cap_is_device cap; ptr = obj_ref_of cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q46 s cap\<rbrace> set_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) 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_ioports 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 cap sa. \<lbrakk>descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref s; pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s; valid_pspace s; 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_ioports 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; idx \<le> 2 ^ cap_bits cap; caps_of_state s cref = Some cap; is_untyped_cap cap; sz = cap_bits cap; dev = cap_is_device cap; ptr = obj_ref_of cap; s = sa\<rbrakk> \<Longrightarrow> ?Q46 s cap sa proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref s; pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s; valid_pspace s; 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_ioports 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; idx \<le> 2 ^ cap_bits cap; caps_of_state s cref = Some cap; is_untyped_cap cap; sz = cap_bits cap; dev = cap_is_device cap; ptr = obj_ref_of cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'68 s cap\<rbrace> set_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) cref \<lbrace>\<lambda>rv s. valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports 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 cap sa. \<lbrakk>descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref s; pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s; valid_pspace s; 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_ioports 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; idx \<le> 2 ^ cap_bits cap; caps_of_state s cref = Some cap; is_untyped_cap cap; sz = cap_bits cap; dev = cap_is_device cap; ptr = obj_ref_of cap; s = sa\<rbrakk> \<Longrightarrow> (valid_mdb sa \<and> valid_pspace sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref sa \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = cap_bits cap \<and> obj_ref_of c = obj_ref_of cap) cref sa \<and> idx \<le> 2 ^ cap_bits cap) \<and> (valid_objs sa \<and> valid_mdb sa \<and> descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref sa \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = cap_bits cap \<and> obj_ref_of c = obj_ref_of cap \<and> cap_is_device c = cap_is_device cap) cref sa) \<and> (valid_ioc and (\<lambda>s. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx = NullCap \<longrightarrow> \<not> is_original_cap s cref)) sa \<and> valid_idle sa \<and> only_idle sa \<and> (cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx))) cref and if_unsafe_then_cap and (\<lambda>s. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx)) cref s)) sa \<and> (valid_reply_caps and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>t rights. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx = 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))) sa \<and> (valid_reply_masters and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>x. (\<exists>rights. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx = ReplyCap x True rights) \<longrightarrow> fst cref = x \<and> snd cref = tcb_cnode_index 2)) sa \<and> (valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) = {})) sa \<and> valid_arch_state sa \<and> ?P'68 s cap sa proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref s; pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s; valid_pspace s; 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; inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s); valid_irq_handlers s; valid_irq_states s; valid_ioports 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; idx \<le> 2 ^ cap_bits cap; caps_of_state s cref = Some cap; is_untyped_cap cap; sz = cap_bits cap; dev = cap_is_device cap; ptr = obj_ref_of cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'68 s cap\<rbrace> set_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) 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_ioports 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 cap sa. \<lbrakk>descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref s; pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s; valid_pspace s; 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_ioports 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; idx \<le> 2 ^ cap_bits cap; caps_of_state s cref = Some cap; is_untyped_cap cap; sz = cap_bits cap; dev = cap_is_device cap; ptr = obj_ref_of cap; s = sa\<rbrakk> \<Longrightarrow> (valid_mdb sa \<and> valid_pspace sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref sa \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = cap_bits cap \<and> obj_ref_of c = obj_ref_of cap) cref sa \<and> idx \<le> 2 ^ cap_bits cap) \<and> (valid_objs sa \<and> valid_mdb sa \<and> descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref sa \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = cap_bits cap \<and> obj_ref_of c = obj_ref_of cap \<and> cap_is_device c = cap_is_device cap) cref sa) \<and> (valid_ioc and (\<lambda>s. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx = NullCap \<longrightarrow> \<not> is_original_cap s cref)) sa \<and> valid_idle sa \<and> only_idle sa \<and> (cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx))) cref and if_unsafe_then_cap and (\<lambda>s. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx)) cref s)) sa \<and> (valid_reply_caps and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>t rights. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx = 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))) sa \<and> (valid_reply_masters and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>x. (\<exists>rights. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx = ReplyCap x True rights) \<longrightarrow> fst cref = x \<and> snd cref = tcb_cnode_index 2)) sa \<and> (valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) = {})) sa \<and> valid_arch_state sa \<and> ?P'68 s cap sa proof (prove)
goal (2 subgoals):
 1. \<And>s cap prev_s. \<lbrakk>descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref s; pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s; valid_pspace s; 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; inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s); valid_irq_handlers s; valid_irq_states s; valid_ioports 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; idx \<le> 2 ^ cap_bits cap; caps_of_state s cref = Some cap; is_untyped_cap cap; sz = cap_bits cap; dev = cap_is_device cap; ptr = obj_ref_of cap\<rbrakk> \<Longrightarrow> \<lbrace>?P71 s cap prev_s\<rbrace> set_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) 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_ioports 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 cap sa. \<lbrakk>descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref s; pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s; valid_pspace s; 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_ioports 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; idx \<le> 2 ^ cap_bits cap; caps_of_state s cref = Some cap; is_untyped_cap cap; sz = cap_bits cap; dev = cap_is_device cap; ptr = obj_ref_of cap; s = sa\<rbrakk> \<Longrightarrow> (valid_mdb sa \<and> valid_pspace sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref sa \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = cap_bits cap \<and> obj_ref_of c = obj_ref_of cap) cref sa \<and> idx \<le> 2 ^ cap_bits cap) \<and> (valid_objs sa \<and> valid_mdb sa \<and> descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref sa \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = cap_bits cap \<and> obj_ref_of c = obj_ref_of cap \<and> cap_is_device c = cap_is_device cap) cref sa) \<and> (valid_ioc and (\<lambda>s. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx = NullCap \<longrightarrow> \<not> is_original_cap s cref)) sa \<and> valid_idle sa \<and> only_idle sa \<and> (cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx))) cref and if_unsafe_then_cap and (\<lambda>s. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx)) cref s)) sa \<and> (valid_reply_caps and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>t rights. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx = 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))) sa \<and> (valid_reply_masters and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>x. (\<exists>rights. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx = ReplyCap x True rights) \<longrightarrow> fst cref = x \<and> snd cref = tcb_cnode_index 2)) sa \<and> (valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) = {})) sa \<and> valid_arch_state sa \<and> ?P71 s cap sa sa proof (prove)
goal (1 subgoal):
 1. \<And>s cap sa. \<lbrakk>descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref s; pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s; valid_pspace s; 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_ioports 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; idx \<le> 2 ^ cap_bits cap; caps_of_state s cref = Some cap; is_untyped_cap cap; sz = cap_bits cap; dev = cap_is_device cap; ptr = obj_ref_of cap; s = sa\<rbrakk> \<Longrightarrow> (valid_mdb sa \<and> valid_pspace sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref sa \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = cap_bits cap \<and> obj_ref_of c = obj_ref_of cap) cref sa \<and> idx \<le> 2 ^ cap_bits cap) \<and> (valid_objs sa \<and> valid_mdb sa \<and> descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref sa \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = cap_bits cap \<and> obj_ref_of c = obj_ref_of cap \<and> cap_is_device c = cap_is_device cap) cref sa) \<and> (valid_ioc and (\<lambda>s. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx = NullCap \<longrightarrow> \<not> is_original_cap s cref)) sa \<and> valid_idle sa \<and> only_idle sa \<and> (cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx))) cref and if_unsafe_then_cap and (\<lambda>s. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx)) cref s)) sa \<and> (valid_reply_caps and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>t rights. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx = 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))) sa \<and> (valid_reply_masters and cte_wp_at (\<lambda>_. True) cref and (\<lambda>s. \<forall>x. (\<exists>rights. UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx = ReplyCap x True rights) \<longrightarrow> fst cref = x \<and> snd cref = tcb_cnode_index 2)) sa \<and> (valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) = {})) sa \<and> valid_arch_state sa \<and> inj (interrupt_irq_node sa) \<and> (\<forall>x. cap_table_at 0 (interrupt_irq_node sa x) sa) \<and> (valid_irq_handlers sa \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) - cap_irqs cap'. irq_issued irq sa) cref sa) \<and> valid_irq_states sa \<and> (valid_ioports sa \<and> cte_wp_at (\<lambda>cap'. safe_ioport_insert (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) cap' sa) cref sa) \<and> valid_machine_state sa \<and> valid_vspace_objs sa \<and> (valid_arch_caps sa \<and> valid_objs sa \<and> cte_wp_at (Not \<circ> is_arch_cap) cref sa \<and> (obj_refs (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<noteq> {} \<longrightarrow> sa \<turnstile> UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<and> \<not> is_arch_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx)) \<and> valid_global_objs sa \<and> valid_kernel_mappings sa \<and> equal_kernel_mappings sa \<and> valid_asid_map sa \<and> valid_global_vspace_mappings sa \<and> pspace_in_kernel_window sa \<and> (cap_refs_in_kernel_window sa \<and> cte_wp_at (\<lambda>cap'. cap_range cap' = cap_range (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx)) cref sa) \<and> pspace_respects_device_region sa \<and> (cap_refs_respects_device_region and (\<lambda>s. \<exists>ptr. cte_wp_at (\<lambda>c. cap_range (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<subseteq> cap_range c \<and> (cap_range (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<noteq> {} \<longrightarrow> cap_is_device (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) = cap_is_device c)) ptr s)) sa \<and> cur_tcb sa proof (prove)
goal (1 subgoal):
 1. \<And>cap sa. \<lbrakk>descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref sa; pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa; valid_pspace sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ cap_bits cap; caps_of_state sa cref = Some cap; is_untyped_cap cap; sz = cap_bits cap; dev = cap_is_device cap; ptr = obj_ref_of cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = cap_bits cap \<and> obj_ref_of c = obj_ref_of cap) cref sa \<and> valid_objs sa \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = cap_bits cap \<and> obj_ref_of c = obj_ref_of cap \<and> cap_is_device c = cap_is_device cap) cref sa \<and> cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx))) cref sa \<and> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx)) cref sa \<and> cte_wp_at (\<lambda>_. True) cref sa \<and> global_refs sa \<inter> {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} = {} \<and> inj (interrupt_irq_node sa) \<and> (\<forall>x. cap_table_at 0 (interrupt_irq_node sa x) sa) \<and> cte_wp_at (\<lambda>cap'. True) cref sa \<and> cte_wp_at (\<lambda>cap'. safe_ioport_insert (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) cap' sa) cref sa \<and> valid_objs sa \<and> cte_wp_at (Not \<circ> is_arch_cap) cref sa \<and> \<not> is_arch_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<and> cte_wp_at (\<lambda>cap'. cap_range cap' = {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1}) cref sa \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} \<subseteq> cap_range c \<and> (obj_ref_of cap \<le> obj_ref_of cap + 2 ^ cap_bits cap - 1 \<longrightarrow> cap_is_device cap = cap_is_device c)) ptr sa) proof (prove)
goal (1 subgoal):
 1. \<And>cap sa. \<lbrakk>descendants_range_in {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} cref sa; pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa; valid_pspace sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ cap_bits cap; caps_of_state sa cref = Some cap; is_untyped_cap cap; sz = cap_bits cap; dev = cap_is_device cap; ptr = obj_ref_of cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = cap_bits cap \<and> obj_ref_of c = obj_ref_of cap) cref sa \<and> valid_objs sa \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = cap_bits cap \<and> obj_ref_of c = obj_ref_of cap \<and> cap_is_device c = cap_is_device cap) cref sa \<and> cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx))) cref sa \<and> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx)) cref sa \<and> cte_wp_at (\<lambda>_. True) cref sa \<and> global_refs sa \<inter> {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} = {} \<and> inj (interrupt_irq_node sa) \<and> (\<forall>x. cap_table_at 0 (interrupt_irq_node sa x) sa) \<and> cte_wp_at (\<lambda>cap'. True) cref sa \<and> cte_wp_at (\<lambda>cap'. safe_ioport_insert (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) cap' sa) cref sa \<and> valid_objs sa \<and> cte_wp_at (Not \<circ> is_arch_cap) cref sa \<and> \<not> is_arch_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<and> cte_wp_at (\<lambda>cap'. cap_range cap' = {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1}) cref sa \<and> cte_wp_at (\<lambda>c. {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} \<subseteq> cap_range c \<and> (obj_ref_of cap \<le> obj_ref_of cap + 2 ^ cap_bits cap - 1 \<longrightarrow> cap_is_device cap = cap_is_device c)) cref sa proof (prove)
goal (1 subgoal):
 1. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> cte_refs (UntypedCap dev ptr sz f) = cte_refs (UntypedCap dev ptr sz idx) \<and> (\<forall>cp. appropriate_cte_cap cp (UntypedCap dev ptr sz f) = appropriate_cte_cap cp (UntypedCap dev ptr sz idx)) \<and> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev ptr sz idx)) cref sa \<and> global_refs sa \<inter> {ptr..ptr + 2 ^ sz - 1} = {} \<and> inj (interrupt_irq_node sa) \<and> (\<forall>x. cap_table_at 0 (interrupt_irq_node sa x) sa) \<and> safe_ioport_insert (UntypedCap dev ptr sz idx) (UntypedCap dev ptr sz f) sa proof (prove)
goal (7 subgoals):
 1. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> cte_refs (UntypedCap dev ptr sz f) = cte_refs (UntypedCap dev ptr sz idx)
 2. \<And>sa f cp. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> appropriate_cte_cap cp (UntypedCap dev ptr sz f) = appropriate_cte_cap cp (UntypedCap dev ptr sz idx)
 3. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev ptr sz idx)) cref sa
 4. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> global_refs sa \<inter> {ptr..ptr + 2 ^ sz - 1} = {}
 5. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node sa)
 6. \<And>sa f x. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> cap_table_at 0 (interrupt_irq_node sa x) sa
 7. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> safe_ioport_insert (UntypedCap dev ptr sz idx) (UntypedCap dev ptr sz f) sa proof (prove)
goal (6 subgoals):
 1. \<And>sa f cp. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> appropriate_cte_cap cp (UntypedCap dev ptr sz f) = appropriate_cte_cap cp (UntypedCap dev ptr sz idx)
 2. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev ptr sz idx)) cref sa
 3. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> global_refs sa \<inter> {ptr..ptr + 2 ^ sz - 1} = {}
 4. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node sa)
 5. \<And>sa f x. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> cap_table_at 0 (interrupt_irq_node sa x) sa
 6. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> safe_ioport_insert (UntypedCap dev ptr sz idx) (UntypedCap dev ptr sz f) sa proof (prove)
goal (5 subgoals):
 1. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev ptr sz idx)) cref sa
 2. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> global_refs sa \<inter> {ptr..ptr + 2 ^ sz - 1} = {}
 3. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node sa)
 4. \<And>sa f x. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> cap_table_at 0 (interrupt_irq_node sa x) sa
 5. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> safe_ioport_insert (UntypedCap dev ptr sz idx) (UntypedCap dev ptr sz f) sa proof (prove)
goal (6 subgoals):
 1. \<And>sa f cap. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa); UntypedCap dev ptr sz f = cap\<rbrakk> \<Longrightarrow> cap \<noteq> NullCap
 2. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa); ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. UntypedCap dev ptr sz f = cap' \<and> appropriate_cte_cap cap' cap) cref sa\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev ptr sz idx)) cref sa
 3. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> global_refs sa \<inter> {ptr..ptr + 2 ^ sz - 1} = {}
 4. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node sa)
 5. \<And>sa f x. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> cap_table_at 0 (interrupt_irq_node sa x) sa
 6. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> safe_ioport_insert (UntypedCap dev ptr sz idx) (UntypedCap dev ptr sz f) sa proof (prove)
goal (5 subgoals):
 1. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa); ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. UntypedCap dev ptr sz f = cap' \<and> appropriate_cte_cap cap' cap) cref sa\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev ptr sz idx)) cref sa
 2. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> global_refs sa \<inter> {ptr..ptr + 2 ^ sz - 1} = {}
 3. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node sa)
 4. \<And>sa f x. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> cap_table_at 0 (interrupt_irq_node sa x) sa
 5. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> safe_ioport_insert (UntypedCap dev ptr sz idx) (UntypedCap dev ptr sz f) sa proof (prove)
goal (4 subgoals):
 1. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> global_refs sa \<inter> {ptr..ptr + 2 ^ sz - 1} = {}
 2. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node sa)
 3. \<And>sa f x. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> cap_table_at 0 (interrupt_irq_node sa x) sa
 4. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> safe_ioport_insert (UntypedCap dev ptr sz idx) (UntypedCap dev ptr sz f) sa proof (prove)
goal (3 subgoals):
 1. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node sa)
 2. \<And>sa f x. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> cap_table_at 0 (interrupt_irq_node sa x) sa
 3. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> safe_ioport_insert (UntypedCap dev ptr sz idx) (UntypedCap dev ptr sz f) sa proof (prove)
goal (2 subgoals):
 1. \<And>sa f x. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> cap_table_at 0 (interrupt_irq_node sa x) sa
 2. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> safe_ioport_insert (UntypedCap dev ptr sz idx) (UntypedCap dev ptr sz f) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_ioports sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; idx \<le> 2 ^ sz; caps_of_state sa cref = Some (UntypedCap dev ptr sz f); valid_objs sa; pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa)\<rbrakk> \<Longrightarrow> safe_ioport_insert (UntypedCap dev ptr sz idx) (UntypedCap dev ptr sz f) sa proof (prove)
goal:
No subgoals!