theory ArchUntyped_AI

lemma set_untyped_cap_invs_simple[Untyped_AI_assms]:
  "\<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> obj_ref_of c = ptr \<and> cap_is_device c = dev) cref s \<and> idx \<le> 2^ sz\<rbrace>
  set_cap (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) 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_untyped_cap_refs_respects_device_simple) apply (clarsimp simp:cte_wp_at_caps_of_state is_cap_simps) apply (intro conjI,clarsimp) apply (rule ext,clarsimp simp:is_cap_simps) 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 simp:no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state vs_cap_ref_def) apply (case_tac cap) apply (simp_all add:vs_cap_ref_def 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 fastforce 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> obj_ref_of c = ptr \<and> cap_is_device c = dev) 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> obj_ref_of c = ptr \<and> cap_is_device c = dev) 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_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; ptr = obj_ref_of cap; dev = cap_is_device 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_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_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; ptr = obj_ref_of cap; dev = cap_is_device cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 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_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_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; ptr = obj_ref_of cap; dev = cap_is_device cap; s = sa\<rbrakk> \<Longrightarrow> ?Q45 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_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; ptr = obj_ref_of cap; dev = cap_is_device cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'67 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_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_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; ptr = obj_ref_of cap; dev = cap_is_device 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'67 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_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; ptr = obj_ref_of cap; dev = cap_is_device cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'67 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_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_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; ptr = obj_ref_of cap; dev = cap_is_device 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'67 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_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; ptr = obj_ref_of cap; dev = cap_is_device cap\<rbrakk> \<Longrightarrow> \<lbrace>?P70 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_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_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; ptr = obj_ref_of cap; dev = cap_is_device 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> ?P70 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_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; ptr = obj_ref_of cap; dev = cap_is_device 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_machine_state sa \<and> valid_vspace_objs sa \<and> (valid_arch_caps sa \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') cref sa \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) = Some vref \<and> obj_refs (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) = obj_refs cap' \<or> \<not> is_final_cap' cap' sa \<and> \<not> reachable_pg_cap cap' sa \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages sa)) \<and> no_cap_to_obj_with_diff_ref (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) {cref} sa \<and> (is_pt_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<or> is_pd_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<longrightarrow> cap_asid (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) = None \<longrightarrow> (\<forall>r\<in>obj_refs (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx). obj_at (empty_table (set (second_level_tables (arch_state sa)))) r sa)) \<and> (is_pt_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<or> is_pd_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<longrightarrow> (\<forall>oldcap. caps_of_state sa cref = Some oldcap \<longrightarrow> is_pt_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<and> is_pt_cap oldcap \<or> is_pd_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx)) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<and> (is_pd_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<and> is_pd_cap cap' \<or> is_pt_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<and> is_pt_cap cap') \<and> (cap_asid (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) = None \<or> cap_asid cap' = None)) ptr' sa \<longrightarrow> ptr' = cref))) \<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 and (\<lambda>s. \<forall>ref\<in>cap_range (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow)) sa \<and> pspace_respects_device_region sa \<and> (K (is_untyped_cap cap) and cte_wp_at ((=) cap) cref and cap_refs_respects_device_region) sa \<and> cur_tcb 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_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_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)\<rbrakk> \<Longrightarrow> valid_objs sa \<and> 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> no_cap_to_obj_with_diff_ref (UntypedCap dev ptr sz idx) {cref} sa \<and> (\<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow) proof (prove)
goal (8 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_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_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)\<rbrakk> \<Longrightarrow> cte_refs (UntypedCap dev ptr sz f) = cte_refs (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_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_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)\<rbrakk> \<Longrightarrow> \<forall>cp. 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_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_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)\<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_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_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)\<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_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_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)\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>x. 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_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_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)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev ptr sz idx) {cref} sa
 8. \<And>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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)\<rbrakk> \<Longrightarrow> \<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>cp. 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_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_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)\<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_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_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)\<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_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_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)\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>x. 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_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_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)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev ptr sz idx) {cref} 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow proof (prove)
goal (6 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_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_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)\<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_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_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)\<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_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_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)\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>x. 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_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_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)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev ptr sz idx) {cref} 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow proof (prove)
goal (7 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_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_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; 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_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_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; 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_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_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)\<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_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_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)\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>x. 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_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_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)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev ptr sz idx) {cref} 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow proof (prove)
goal (6 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_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_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; 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_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_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)\<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_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_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)\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>x. 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_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_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)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev ptr sz idx) {cref} 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow 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_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_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)\<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_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_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)\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>x. 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_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_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)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap dev ptr sz idx) {cref} 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow 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_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_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)\<rbrakk> \<Longrightarrow> inj (interrupt_irq_node 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>x. 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_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_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)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (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_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_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)\<rbrakk> \<Longrightarrow> \<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>x. 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_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_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)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (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_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_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)\<rbrakk> \<Longrightarrow> \<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow proof (prove)
goal (2 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_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_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)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (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_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_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)\<rbrakk> \<Longrightarrow> \<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow proof (prove)
goal (2 subgoals):
 1. \<And>sa f a b cap. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; obj_refs cap = {}; caps_of_state sa (a, b) = Some cap\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (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_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_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)\<rbrakk> \<Longrightarrow> \<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow proof (prove)
goal (13 subgoals):
 1. \<And>sa f a b cap. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; obj_refs cap = {}; caps_of_state sa (a, b) = Some cap; cap = NullCap\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (UntypedCap dev ptr sz idx)
 2. \<And>sa f a b cap x21 x22 x23 x24. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; obj_refs cap = {}; caps_of_state sa (a, b) = Some cap; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (UntypedCap dev ptr sz idx)
 3. \<And>sa f a b cap x31 x32 x33. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; obj_refs cap = {}; caps_of_state sa (a, b) = Some cap; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (UntypedCap dev ptr sz idx)
 4. \<And>sa f a b cap x41 x42 x43. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; obj_refs cap = {}; caps_of_state sa (a, b) = Some cap; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (UntypedCap dev ptr sz idx)
 5. \<And>sa f a b cap x51 x52 x53. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; obj_refs cap = {}; caps_of_state sa (a, b) = Some cap; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (UntypedCap dev ptr sz idx)
 6. \<And>sa f a b cap x61 x62 x63. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; obj_refs cap = {}; caps_of_state sa (a, b) = Some cap; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (UntypedCap dev ptr sz idx)
 7. \<And>sa f a b cap x7. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; obj_refs cap = {}; caps_of_state sa (a, b) = Some cap; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (UntypedCap dev ptr sz idx)
 8. \<And>sa f a b cap. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; obj_refs cap = {}; caps_of_state sa (a, b) = Some cap; cap = DomainCap\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (UntypedCap dev ptr sz idx)
 9. \<And>sa f a b cap. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; obj_refs cap = {}; caps_of_state sa (a, b) = Some cap; cap = IRQControlCap\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (UntypedCap dev ptr sz idx)
 10. \<And>sa f a b cap x10. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; obj_refs cap = {}; caps_of_state sa (a, b) = Some cap; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (UntypedCap dev ptr sz idx)
A total of 13 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>sa f a b cap x12. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; aobj_ref x12 = None; caps_of_state sa (a, b) = Some (ArchObjectCap x12); cap = 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>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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)\<rbrakk> \<Longrightarrow> \<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow proof (prove)
goal (2 subgoals):
 1. \<And>sa f a b cap arch_cap. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; aobj_ref arch_cap = None; caps_of_state sa (a, b) = Some (ArchObjectCap arch_cap); cap = 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>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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)\<rbrakk> \<Longrightarrow> \<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow proof (prove)
goal (6 subgoals):
 1. \<And>sa f a b cap arch_cap x11 x12. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; aobj_ref arch_cap = None; caps_of_state sa (a, b) = Some (ArchObjectCap arch_cap); cap = 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>sa f a b cap arch_cap. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; aobj_ref arch_cap = None; caps_of_state sa (a, b) = Some (ArchObjectCap arch_cap); cap = 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>sa f a b cap arch_cap x31 x32 x33 x34 x35. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; aobj_ref arch_cap = None; caps_of_state sa (a, b) = Some (ArchObjectCap arch_cap); cap = 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>sa f a b cap arch_cap x41 x42. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; aobj_ref arch_cap = None; caps_of_state sa (a, b) = Some (ArchObjectCap arch_cap); cap = 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>sa f a b cap arch_cap x51 x52. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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); (a, b) \<noteq> cref; aobj_ref arch_cap = None; caps_of_state sa (a, b) = Some (ArchObjectCap arch_cap); cap = 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>sa f. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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)\<rbrakk> \<Longrightarrow> \<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow 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_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_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)\<rbrakk> \<Longrightarrow> \<forall>ref\<in>{ptr..ptr + 2 ^ sz - 1}. arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<And>sa f ref. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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; \<forall>cref. \<not> cte_wp_at (\<lambda>c. {x. arm_kernel_vspace (arch_state sa) x \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range c \<noteq> {}) cref 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); ptr \<le> ref; ref \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<And>sa f ref. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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; 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); ptr \<le> ref; ref \<le> ptr + 2 ^ sz - 1; \<not> cte_wp_at (\<lambda>c. {x. arm_kernel_vspace (arch_state sa) x \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range c \<noteq> {}) cref sa\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<And>sa f ref. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref sa; pspace_no_overlap (up_aligned_area ptr sz) 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_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; 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); ptr \<le> ref; ref \<le> ptr + 2 ^ sz - 1; {x. arm_kernel_vspace (arch_state sa) x \<noteq> ArmVSpaceKernelWindow} \<inter> {ptr..ptr + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state sa) ref = ArmVSpaceKernelWindow proof (prove)
goal:
No subgoals!