theory ArchVSpace_AI

lemma arch_update_cap_invs_map:
  "\<lbrace>cte_wp_at (is_arch_update cap and
               (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> vs_cap_ref cap = Some r)) p
             and invs and valid_cap cap\<rbrace>
  set_cap cap p
  \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: invs_def valid_state_def) apply (rule hoare_pre) apply (wp arch_update_cap_pspace arch_update_cap_valid_mdb set_cap_idle
             update_cap_ifunsafe valid_irq_node_typ set_cap_typ_at
             set_cap_irq_handlers set_cap_valid_arch_caps
             set_cap_cap_refs_respects_device_region_spec[where ptr = p]) apply (clarsimp simp: cte_wp_at_caps_of_state
              simp del: imp_disjL) apply (frule(1) valid_global_refsD2) apply (frule(1) cap_refs_in_kernel_windowD) apply (clarsimp simp: is_cap_simps is_arch_update_def
              simp del: imp_disjL) apply (frule master_cap_cap_range, simp del: imp_disjL) apply (thin_tac "cap_range a = cap_range b" for a b) apply (rule conjI) apply (fastforce simp:is_valid_vtable_root_def vs_cap_ref_def split:arch_cap.splits vmpage_size.splits option.splits) apply (rule conjI) apply (rule ext) apply (simp add: cap_master_cap_def split: cap.splits arch_cap.splits) apply (rule context_conjI) apply (simp add: appropriate_cte_cap_irqs) apply (clarsimp simp: cap_irqs_def cap_irq_opt_def cap_master_cap_def
                  split: cap.split) apply (rule conjI) apply (drule(1) if_unsafe_then_capD [OF caps_of_state_cteD]) apply (clarsimp simp: cap_master_cap_def) apply (erule ex_cte_cap_wp_to_weakenE) apply (clarsimp simp: appropriate_cte_cap_def cap_master_cap_def
                  split: cap.split_asm) apply (rule conjI) apply (frule master_cap_obj_refs) apply simp apply (rule conjI) apply (frule master_cap_obj_refs) apply (case_tac "table_cap_ref capa =
                    table_cap_ref (ArchObjectCap a)") apply (frule unique_table_refs_no_cap_asidE[where S="{p}"]) apply (simp add: valid_arch_caps_def) apply (simp add: no_cap_to_obj_with_diff_ref_def Ball_def) apply (case_tac "table_cap_ref capa") apply clarsimp apply (erule no_cap_to_obj_with_diff_ref_map,
           simp_all)[1] apply (clarsimp simp: table_cap_ref_def cap_master_cap_simps
                            is_cap_simps
                     split: cap.split_asm arch_cap.split_asm
                     dest!: cap_master_cap_eqDs) apply (simp add: valid_arch_caps_def) apply (simp add: valid_pspace_def) apply (erule swap) apply (erule vs_cap_ref_eq_imp_table_cap_ref_eq'[symmetric]) apply (frule table_cap_ref_vs_cap_ref_Some) apply simp apply (rule conjI) apply (clarsimp simp del: imp_disjL) apply (erule disjE) apply (clarsimp simp: is_pt_cap_def cap_master_cap_simps
                          cap_asid_def vs_cap_ref_def
                   dest!: cap_master_cap_eqDs split: option.split_asm prod.split_asm) apply (drule valid_table_capsD[OF caps_of_state_cteD]) apply (clarsimp simp: invs_def valid_state_def valid_arch_caps_def) apply (simp add: is_pt_cap_def) apply (simp add: cap_asid_def) apply simp apply (clarsimp simp: is_cap_simps cap_master_cap_simps
                          cap_asid_def vs_cap_ref_def
                   dest!: cap_master_cap_eqDs split: option.split_asm prod.split_asm) apply (drule valid_table_capsD[OF caps_of_state_cteD]) apply (clarsimp simp: invs_def valid_state_def valid_arch_caps_def) apply (simp add: is_cap_simps) apply (simp add: cap_asid_def) apply simp apply (clarsimp simp: is_cap_simps is_pt_cap_def cap_master_cap_simps
                        cap_asid_def vs_cap_ref_def ranI
                 dest!: cap_master_cap_eqDs split: option.split_asm if_split_asm
                 elim!: ranE cong: master_cap_eq_is_device_cap_eq
             | rule conjI)+ apply (clarsimp dest!: master_cap_eq_is_device_cap_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (is_arch_update cap and (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> vs_cap_ref cap = Some r)) p and invs and valid_cap cap\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (is_arch_update cap and (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> vs_cap_ref cap = Some r)) p and (valid_pspace and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) and valid_cap cap\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_pspace and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_pspace and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace>
 2. \<And>s. (cte_wp_at (is_arch_update cap and (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> vs_cap_ref cap = Some r)) p and (valid_pspace and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) and valid_cap cap) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at (is_arch_update cap and (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> vs_cap_ref cap = Some r)) p and (valid_pspace and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) and valid_cap cap) s \<Longrightarrow> (cte_wp_at (is_arch_update cap and (\<lambda>c. is_valid_vtable_root c \<longrightarrow> is_valid_vtable_root cap)) p and valid_pspace and valid_cap cap) s \<and> (cte_wp_at (is_arch_update cap) p and valid_mdb) s \<and> (valid_ioc and (\<lambda>s. cap = NullCap \<longrightarrow> \<not> is_original_cap s p)) s \<and> valid_idle s \<and> only_idle s \<and> (cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs cap \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp cap)) p and if_unsafe_then_cap and (\<lambda>s. cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)) s \<and> (valid_reply_caps and cte_wp_at (\<lambda>_. True) p and (\<lambda>s. \<forall>t rights. cap = ReplyCap t False rights \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (\<not> has_reply_cap t s \<or> cte_wp_at (is_reply_cap_to t) p s))) s \<and> (valid_reply_masters and cte_wp_at (\<lambda>_. True) p and (\<lambda>s. \<forall>x. (\<exists>rights. cap = ReplyCap x True rights) \<longrightarrow> fst p = x \<and> snd p = tcb_cnode_index 2)) s \<and> (valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range cap = {})) s \<and> valid_arch_state s \<and> valid_irq_node s \<and> (valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) p s) \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> (valid_arch_caps s \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') p s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {p} s \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s p = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = p))) \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> (cap_refs_in_kernel_window and (\<lambda>s. \<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow)) s \<and> pspace_respects_device_region s \<and> (cap_refs_respects_device_region and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device c)) p) s \<and> cur_tcb s proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; is_arch_update cap capa; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref cap = Some r; 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; s \<turnstile> cap\<rbrakk> \<Longrightarrow> (is_valid_vtable_root capa \<longrightarrow> is_valid_vtable_root cap) \<and> (cap = NullCap \<longrightarrow> \<not> is_original_cap s p) \<and> cte_refs capa = cte_refs cap \<and> (\<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp cap) \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s) \<and> (\<forall>t. (\<exists>rights. cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (has_reply_cap t s \<longrightarrow> is_reply_cap_to t capa)) \<and> (\<forall>x. (\<exists>rights. cap = ReplyCap x True rights) \<longrightarrow> fst p = x \<and> snd p = tcb_cnode_index 2) \<and> global_refs s \<inter> cap_range cap = {} \<and> (\<forall>irq\<in>cap_irqs cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> obj_refs cap = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {p} s \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap capa \<or> is_pd_cap cap \<and> is_pd_cap capa \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> obj_refs cap) \<longrightarrow> (\<forall>a b. (\<exists>capa. caps_of_state s (a, b) = Some capa \<and> obj_refs capa = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap capa \<or> is_pt_cap cap \<and> is_pt_cap capa) \<and> (cap_asid cap = None \<or> cap_asid capa = None)) \<longrightarrow> (a, b) = p)) \<and> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range cap \<subseteq> cap_range capa \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; is_arch_update cap capa; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref cap = Some r; 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; s \<turnstile> cap; global_refs s \<inter> cap_range capa = {}\<rbrakk> \<Longrightarrow> (is_valid_vtable_root capa \<longrightarrow> is_valid_vtable_root cap) \<and> (cap = NullCap \<longrightarrow> \<not> is_original_cap s p) \<and> cte_refs capa = cte_refs cap \<and> (\<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp cap) \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s) \<and> (\<forall>t. (\<exists>rights. cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (has_reply_cap t s \<longrightarrow> is_reply_cap_to t capa)) \<and> (\<forall>x. (\<exists>rights. cap = ReplyCap x True rights) \<longrightarrow> fst p = x \<and> snd p = tcb_cnode_index 2) \<and> global_refs s \<inter> cap_range cap = {} \<and> (\<forall>irq\<in>cap_irqs cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> obj_refs cap = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {p} s \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap capa \<or> is_pd_cap cap \<and> is_pd_cap capa \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> obj_refs cap) \<longrightarrow> (\<forall>a b. (\<exists>capa. caps_of_state s (a, b) = Some capa \<and> obj_refs capa = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap capa \<or> is_pt_cap cap \<and> is_pt_cap capa) \<and> (cap_asid cap = None \<or> cap_asid capa = None)) \<longrightarrow> (a, b) = p)) \<and> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range cap \<subseteq> cap_range capa \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; is_arch_update cap capa; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref cap = Some r; 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; s \<turnstile> cap; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> (is_valid_vtable_root capa \<longrightarrow> is_valid_vtable_root cap) \<and> (cap = NullCap \<longrightarrow> \<not> is_original_cap s p) \<and> cte_refs capa = cte_refs cap \<and> (\<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp cap) \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s) \<and> (\<forall>t. (\<exists>rights. cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (has_reply_cap t s \<longrightarrow> is_reply_cap_to t capa)) \<and> (\<forall>x. (\<exists>rights. cap = ReplyCap x True rights) \<longrightarrow> fst p = x \<and> snd p = tcb_cnode_index 2) \<and> global_refs s \<inter> cap_range cap = {} \<and> (\<forall>irq\<in>cap_irqs cap - cap_irqs capa. irq_issued irq s) \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> obj_refs cap = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {p} s \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap capa \<or> is_pd_cap cap \<and> is_pd_cap capa \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> obj_refs cap) \<longrightarrow> (\<forall>a b. (\<exists>capa. caps_of_state s (a, b) = Some capa \<and> obj_refs capa = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap capa \<or> is_pt_cap cap \<and> is_pt_cap capa) \<and> (cap_asid cap = None \<or> cap_asid capa = None)) \<longrightarrow> (a, b) = p)) \<and> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range cap \<subseteq> cap_range capa \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a\<rbrakk> \<Longrightarrow> (is_valid_vtable_root capa \<longrightarrow> is_valid_vtable_root (ArchObjectCap a)) \<and> cte_refs capa = cte_refs (ArchObjectCap a) \<and> (\<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)) \<and> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap a)) p s \<and> global_refs s \<inter> cap_range (ArchObjectCap a) = {} \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (\<forall>ref\<in>cap_range (ArchObjectCap a). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap a) \<subseteq> cap_range capa \<and> (cap_range (ArchObjectCap a) \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; cap_range (ArchObjectCap a) = cap_range capa\<rbrakk> \<Longrightarrow> (is_valid_vtable_root capa \<longrightarrow> is_valid_vtable_root (ArchObjectCap a)) \<and> cte_refs capa = cte_refs (ArchObjectCap a) \<and> (\<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)) \<and> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap a)) p s \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a\<rbrakk> \<Longrightarrow> (is_valid_vtable_root capa \<longrightarrow> is_valid_vtable_root (ArchObjectCap a)) \<and> cte_refs capa = cte_refs (ArchObjectCap a) \<and> (\<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)) \<and> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap a)) p s \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a\<rbrakk> \<Longrightarrow> is_valid_vtable_root capa \<longrightarrow> is_valid_vtable_root (ArchObjectCap a)
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a\<rbrakk> \<Longrightarrow> cte_refs capa = cte_refs (ArchObjectCap a) \<and> (\<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)) \<and> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap a)) p s \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a\<rbrakk> \<Longrightarrow> cte_refs capa = cte_refs (ArchObjectCap a) \<and> (\<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)) \<and> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap a)) p s \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a\<rbrakk> \<Longrightarrow> cte_refs capa = cte_refs (ArchObjectCap a)
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a\<rbrakk> \<Longrightarrow> (\<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)) \<and> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap a)) p s \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a x. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a\<rbrakk> \<Longrightarrow> cte_refs capa x = cte_refs (ArchObjectCap a) x
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a\<rbrakk> \<Longrightarrow> (\<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)) \<and> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap a)) p s \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a\<rbrakk> \<Longrightarrow> (\<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)) \<and> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap a)) p s \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a\<rbrakk> \<Longrightarrow> \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap a)) p s \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a\<rbrakk> \<Longrightarrow> cap_irqs capa = {}
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap a)) p s \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap a)) p s \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap a)) p s
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (3 subgoals):
 1. \<And>s capa a capaa. \<lbrakk>valid_pspace s; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); capa = capaa\<rbrakk> \<Longrightarrow> capaa \<noteq> NullCap
 2. \<And>s capa a. \<lbrakk>valid_pspace s; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. capa = cap' \<and> appropriate_cte_cap cap' cap) p s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap a)) p s
 3. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. capa = cap' \<and> appropriate_cte_cap cap' cap) p s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap a)) p s
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a cte_cap. \<lbrakk>valid_pspace s; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); \<exists>cap'. capa = cap' \<and> appropriate_cte_cap cap' cte_cap; p \<in> cte_refs cte_cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> appropriate_cte_cap (ArchObjectCap a) cte_cap
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> \<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa\<rbrakk> \<Longrightarrow> \<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> set_option (aobj_ref a) = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (3 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa = table_cap_ref (ArchObjectCap a)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa \<noteq> table_cap_ref (ArchObjectCap a)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 3. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (4 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa = table_cap_ref (ArchObjectCap a)\<rbrakk> \<Longrightarrow> unique_table_refs (caps_of_state s)
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa = table_cap_ref (ArchObjectCap a); no_cap_to_obj_with_diff_ref capa {p} s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 3. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa \<noteq> table_cap_ref (ArchObjectCap a)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 4. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (3 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa = table_cap_ref (ArchObjectCap a); no_cap_to_obj_with_diff_ref capa {p} s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa \<noteq> table_cap_ref (ArchObjectCap a)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 3. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa \<noteq> table_cap_ref (ArchObjectCap a)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (3 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa \<noteq> table_cap_ref (ArchObjectCap a); table_cap_ref capa = None\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 2. \<And>s capa a aa. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa \<noteq> table_cap_ref (ArchObjectCap a); table_cap_ref capa = Some aa\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 3. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (3 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); set_option (aobj_ref a) = obj_refs capa; None \<noteq> table_cap_ref (ArchObjectCap a); table_cap_ref capa = None\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 2. \<And>s capa a aa. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa \<noteq> table_cap_ref (ArchObjectCap a); table_cap_ref capa = Some aa\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 3. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (5 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); set_option (aobj_ref a) = obj_refs capa; None \<noteq> table_cap_ref (ArchObjectCap a); table_cap_ref capa = None\<rbrakk> \<Longrightarrow> is_pt_cap capa \<or> is_pd_cap capa
 2. \<And>s capa a. \<lbrakk>valid_pspace s; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); set_option (aobj_ref a) = obj_refs capa; None \<noteq> table_cap_ref (ArchObjectCap a); table_cap_ref capa = None\<rbrakk> \<Longrightarrow> unique_table_caps (caps_of_state s)
 3. \<And>s capa a. \<lbrakk>valid_pspace s; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); set_option (aobj_ref a) = obj_refs capa; None \<noteq> table_cap_ref (ArchObjectCap a); table_cap_ref capa = None\<rbrakk> \<Longrightarrow> valid_objs s
 4. \<And>s capa a aa. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa \<noteq> table_cap_ref (ArchObjectCap a); table_cap_ref capa = Some aa\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 5. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (4 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); set_option (aobj_ref a) = obj_refs capa; None \<noteq> table_cap_ref (ArchObjectCap a); table_cap_ref capa = None\<rbrakk> \<Longrightarrow> unique_table_caps (caps_of_state s)
 2. \<And>s capa a. \<lbrakk>valid_pspace s; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); set_option (aobj_ref a) = obj_refs capa; None \<noteq> table_cap_ref (ArchObjectCap a); table_cap_ref capa = None\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<And>s capa a aa. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa \<noteq> table_cap_ref (ArchObjectCap a); table_cap_ref capa = Some aa\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 4. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (3 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); set_option (aobj_ref a) = obj_refs capa; None \<noteq> table_cap_ref (ArchObjectCap a); table_cap_ref capa = None\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s capa a aa. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa \<noteq> table_cap_ref (ArchObjectCap a); table_cap_ref capa = Some aa\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 3. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a aa. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa \<noteq> table_cap_ref (ArchObjectCap a); table_cap_ref capa = Some aa\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a aa. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa = Some aa; \<not> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref (ArchObjectCap a)
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a aa. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa = Some aa; \<not> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s\<rbrakk> \<Longrightarrow> vs_cap_ref (ArchObjectCap a) = vs_cap_ref capa
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a aa. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); obj_refs (ArchObjectCap a) = obj_refs capa; table_cap_ref capa = Some aa; \<not> no_cap_to_obj_with_diff_ref (ArchObjectCap a) {p} s; vs_cap_ref capa = Some aa\<rbrakk> \<Longrightarrow> vs_cap_ref (ArchObjectCap a) = vs_cap_ref capa
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> (\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap a) = None \<longrightarrow> (\<forall>r\<in>set_option (aobj_ref a). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a r. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); (\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid); cap_asid (ArchObjectCap a) = None; aobj_ref a = Some r\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (3 subgoals):
 1. \<And>s capa a r. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); cap_asid (ArchObjectCap a) = None; aobj_ref a = Some r; \<exists>p asid. a = PageTableCap p asid\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 2. \<And>s capa a r. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); cap_asid (ArchObjectCap a) = None; aobj_ref a = Some r; \<exists>p asid. a = PageDirectoryCap p asid\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 3. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (3 subgoals):
 1. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageTableCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageTableCap r None); valid_pspace s; caps_of_state s p = Some (ArchObjectCap (PageTableCap r None)); valid_mdb s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 2. \<And>s capa a r. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); cap_asid (ArchObjectCap a) = None; aobj_ref a = Some r; \<exists>p asid. a = PageDirectoryCap p asid\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 3. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (6 subgoals):
 1. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageTableCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageTableCap r None); valid_pspace s; valid_mdb s\<rbrakk> \<Longrightarrow> valid_table_caps s
 2. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageTableCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageTableCap r None); valid_pspace s; valid_mdb s\<rbrakk> \<Longrightarrow> is_pt_cap (ArchObjectCap (PageTableCap r None)) \<or> is_pd_cap (ArchObjectCap (PageTableCap r None))
 3. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageTableCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageTableCap r None); valid_pspace s; valid_mdb s\<rbrakk> \<Longrightarrow> cap_asid (ArchObjectCap (PageTableCap r None)) = None
 4. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageTableCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageTableCap r None); valid_pspace s; valid_mdb s; \<forall>r\<in>obj_refs (ArchObjectCap (PageTableCap r None)). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 5. \<And>s capa a r. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); cap_asid (ArchObjectCap a) = None; aobj_ref a = Some r; \<exists>p asid. a = PageDirectoryCap p asid\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 6. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (5 subgoals):
 1. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageTableCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageTableCap r None); valid_pspace s; valid_mdb s\<rbrakk> \<Longrightarrow> is_pt_cap (ArchObjectCap (PageTableCap r None)) \<or> is_pd_cap (ArchObjectCap (PageTableCap r None))
 2. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageTableCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageTableCap r None); valid_pspace s; valid_mdb s\<rbrakk> \<Longrightarrow> cap_asid (ArchObjectCap (PageTableCap r None)) = None
 3. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageTableCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageTableCap r None); valid_pspace s; valid_mdb s; \<forall>r\<in>obj_refs (ArchObjectCap (PageTableCap r None)). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 4. \<And>s capa a r. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); cap_asid (ArchObjectCap a) = None; aobj_ref a = Some r; \<exists>p asid. a = PageDirectoryCap p asid\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 5. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (4 subgoals):
 1. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageTableCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageTableCap r None); valid_pspace s; valid_mdb s\<rbrakk> \<Longrightarrow> cap_asid (ArchObjectCap (PageTableCap r None)) = None
 2. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageTableCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageTableCap r None); valid_pspace s; valid_mdb s; \<forall>r\<in>obj_refs (ArchObjectCap (PageTableCap r None)). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 3. \<And>s capa a r. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); cap_asid (ArchObjectCap a) = None; aobj_ref a = Some r; \<exists>p asid. a = PageDirectoryCap p asid\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 4. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (3 subgoals):
 1. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageTableCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageTableCap r None); valid_pspace s; valid_mdb s; \<forall>r\<in>obj_refs (ArchObjectCap (PageTableCap r None)). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 2. \<And>s capa a r. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); cap_asid (ArchObjectCap a) = None; aobj_ref a = Some r; \<exists>p asid. a = PageDirectoryCap p asid\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 3. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a r. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); cap_asid (ArchObjectCap a) = None; aobj_ref a = Some r; \<exists>p asid. a = PageDirectoryCap p asid\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageDirectoryCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageDirectoryCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageDirectoryCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageDirectoryCap r None); valid_pspace s; caps_of_state s p = Some (ArchObjectCap (PageDirectoryCap r None)); valid_mdb s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (5 subgoals):
 1. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageDirectoryCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageDirectoryCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageDirectoryCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageDirectoryCap r None); valid_pspace s; valid_mdb s\<rbrakk> \<Longrightarrow> valid_table_caps s
 2. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageDirectoryCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageDirectoryCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageDirectoryCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageDirectoryCap r None); valid_pspace s; valid_mdb s\<rbrakk> \<Longrightarrow> is_pt_cap (ArchObjectCap (PageDirectoryCap r None)) \<or> is_pd_cap (ArchObjectCap (PageDirectoryCap r None))
 3. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageDirectoryCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageDirectoryCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageDirectoryCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageDirectoryCap r None); valid_pspace s; valid_mdb s\<rbrakk> \<Longrightarrow> cap_asid (ArchObjectCap (PageDirectoryCap r None)) = None
 4. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageDirectoryCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageDirectoryCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageDirectoryCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageDirectoryCap r None); valid_pspace s; valid_mdb s; \<forall>r\<in>obj_refs (ArchObjectCap (PageDirectoryCap r None)). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 5. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (4 subgoals):
 1. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageDirectoryCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageDirectoryCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageDirectoryCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageDirectoryCap r None); valid_pspace s; valid_mdb s\<rbrakk> \<Longrightarrow> is_pt_cap (ArchObjectCap (PageDirectoryCap r None)) \<or> is_pd_cap (ArchObjectCap (PageDirectoryCap r None))
 2. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageDirectoryCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageDirectoryCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageDirectoryCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageDirectoryCap r None); valid_pspace s; valid_mdb s\<rbrakk> \<Longrightarrow> cap_asid (ArchObjectCap (PageDirectoryCap r None)) = None
 3. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageDirectoryCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageDirectoryCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageDirectoryCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageDirectoryCap r None); valid_pspace s; valid_mdb s; \<forall>r\<in>obj_refs (ArchObjectCap (PageDirectoryCap r None)). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 4. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (3 subgoals):
 1. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageDirectoryCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageDirectoryCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageDirectoryCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageDirectoryCap r None); valid_pspace s; valid_mdb s\<rbrakk> \<Longrightarrow> cap_asid (ArchObjectCap (PageDirectoryCap r None)) = None
 2. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageDirectoryCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageDirectoryCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageDirectoryCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageDirectoryCap r None); valid_pspace s; valid_mdb s; \<forall>r\<in>obj_refs (ArchObjectCap (PageDirectoryCap r None)). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 3. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s r. \<lbrakk>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; s \<turnstile> ArchObjectCap (PageDirectoryCap r None); global_refs s \<inter> cap_range (ArchObjectCap (PageDirectoryCap r None)) = {}; \<forall>ref\<in>cap_range (ArchObjectCap (PageDirectoryCap r None)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap = ArchObjectCap (PageDirectoryCap r None); valid_pspace s; valid_mdb s; \<forall>r\<in>obj_refs (ArchObjectCap (PageDirectoryCap r None)). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s
 2. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref (ArchObjectCap a) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<longrightarrow> ((\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. capa = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (cap_asid (ArchObjectCap a) = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> set_option (aobj_ref a)) \<longrightarrow> (\<forall>aa b. (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> obj_refs cap = set_option (aobj_ref a) \<and> ((\<exists>p asid. a = PageDirectoryCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<or> (\<exists>p asid. a = PageTableCap p asid) \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> (cap_asid (ArchObjectCap a) = None \<or> cap_asid cap = None)) \<longrightarrow> (aa, b) = p)) \<and> (cap_range capa \<noteq> {} \<longrightarrow> arch_cap_is_device a = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a. \<lbrakk>valid_pspace s; caps_of_state s p = Some capa; valid_mdb s; \<forall>r. (case capa of ArchObjectCap (ASIDPoolCap obj_ref asid) \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap ASIDControlCap \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights ARMSection None) \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights ARMSection (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] | ArchObjectCap (PageCap dev obj_ref rights ARMSuperSection None) \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights ARMSuperSection (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] | ArchObjectCap (PageCap dev obj_ref rights _ None) \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights _ (Some (asid, vptr))) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | ArchObjectCap (PageTableCap obj_ref None) \<Rightarrow> None | ArchObjectCap (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] | ArchObjectCap (PageDirectoryCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageDirectoryCap obj_ref (Some asida)) \<Rightarrow> Some [VSRef (asida && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asida)) None] | _ \<Rightarrow> None) = Some r \<longrightarrow> (case a of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | 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]) = Some r; 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; s \<turnstile> ArchObjectCap a; global_refs s \<inter> cap_range capa = {}; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow; cap_master_cap (ArchObjectCap a) = cap_master_cap capa; cap = ArchObjectCap a; \<forall>cp. appropriate_cte_cap cp capa = appropriate_cte_cap cp (ArchObjectCap a); cap_range capa \<noteq> {}\<rbrakk> \<Longrightarrow> arch_cap_is_device a = cap_is_device capa proof (prove)
goal:
No subgoals!