theory ArchArch_AC

lemma perform_asid_control_invocation_pas_refined [wp]:
  "\<lbrace>pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active
                    and K (authorised_asid_control_inv aag aci)\<rbrace>
   perform_asid_control_invocation aci
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: perform_asid_control_invocation_def) apply (rule hoare_pre) apply (wp cap_insert_pas_refined' hoare_weak_lift_imp
          | strengthen pas_refined_set_asid_strg
          | wpc
          | simp add: delete_objects_def2 fun_upd_def[symmetric])+ apply (wp retype_region_pas_refined'[where sz=pageBits]
                hoare_vcg_ex_lift hoare_vcg_all_lift hoare_weak_lift_imp hoare_wp_combs hoare_drop_imp
                retype_region_invs_extras(1)[where sz = pageBits]
                retype_region_invs_extras(4)[where sz = pageBits]
                retype_region_invs_extras(6)[where sz = pageBits]
                retype_region_invs_extras(7)[where sz = pageBits]
             | simp add: do_machine_op_def split_def cte_wp_at_neg2)+ apply (wp retype_region_cte_at_other'[where sz=pageBits]
                max_index_upd_invs_simple max_index_upd_caps_overlap_reserved
                hoare_vcg_ex_lift set_cap_cte_wp_at hoare_vcg_disj_lift set_free_index_valid_pspace
                set_cap_descendants_range_in set_cap_no_overlap get_cap_wp set_cap_caps_no_overlap
                hoare_vcg_all_lift hoare_weak_lift_imp retype_region_invs_extras
                set_cap_pas_refined_not_transferable
             | simp add: do_machine_op_def split_def cte_wp_at_neg2 region_in_kernel_window_def)+ apply (rename_tac frame slot parent base cap) apply (case_tac slot, rename_tac slot_ptr slot_idx) apply (case_tac parent, rename_tac parent_ptr parent_idx) apply (rule_tac Q="\<lambda>rv s.
             (\<exists>idx. cte_wp_at ((=) (UntypedCap False frame pageBits idx)) parent s) \<and>
             (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and>
             pas_refined aag s \<and>
             pas_cur_domain aag s \<and>
             pspace_no_overlap_range_cover frame pageBits s \<and>
             invs s \<and>
             descendants_range_in
               {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} parent s \<and>
             range_cover frame pageBits
               (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and>
             is_subject aag slot_ptr \<and>
             is_subject aag parent_ptr \<and>
             pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and>
             is_subject aag frame \<and>
             (\<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow>
                 is_subject_asid aag x)"
             in hoare_strengthen_post) apply (simp add: page_bits_def) apply (wp add: delete_objects_pspace_no_overlap hoare_vcg_ex_lift
                   delete_objects_descendants_range_in delete_objects_invs_ex
                   delete_objects_pas_refined
              del: Untyped_AI.delete_objects_pspace_no_overlap
           | simp add: page_bits_def)+ apply clarsimp apply (rename_tac s idx) apply (frule untyped_cap_aligned, simp add: invs_valid_objs) apply (clarsimp simp: cte_wp_at_def aag_cap_auth_def ptr_range_def pas_refined_refl
                         cap_links_asid_slot_def cap_links_irq_def obj_bits_api_def
                         invs_psp_aligned invs_vspace_objs invs_arch_state invs_strgs
                         default_arch_object_def retype_addrs_def cong: conj_cong) apply (rule conjI, force intro: descendants_range_caps_no_overlapI
                             simp: cte_wp_at_def) apply (rule conjI) apply (cut_tac s=s and ptr="(parent_ptr, parent_idx)" in cap_refs_in_kernel_windowD) apply ((fastforce simp add: caps_of_state_def cap_range_def)+)[3] apply (rule conjI, force simp: field_simps) apply (fastforce dest: caps_of_state_valid
                    simp: caps_of_state_def free_index_of_def max_free_index_def valid_cap_def) apply (clarsimp simp: valid_aci_def authorised_asid_control_inv_def) apply (rename_tac frame slot_ptr slot_idx parent_ptr parent_idx base) apply (subgoal_tac "is_aligned frame pageBits") apply (clarsimp simp: cte_wp_at_caps_of_state) apply (rule conjI) apply (drule untyped_slots_not_in_untyped_range) apply (erule empty_descendants_range_in) apply (simp add: cte_wp_at_caps_of_state) apply simp apply (rule refl) apply (rule subset_refl) apply (simp add: page_bits_def) apply (clarsimp simp: ptr_range_def invs_psp_aligned invs_valid_objs
                         descendants_range_def2 empty_descendants_range_in page_bits_def) apply ((strengthen refl | simp)+)? apply (rule conjI, fastforce) apply (rule conjI, fastforce intro: empty_descendants_range_in) apply (rule conjI) apply (clarsimp simp: range_cover_def obj_bits_api_def default_arch_object_def) apply (subst is_aligned_neg_mask_eq[THEN sym], assumption) apply (simp add: and_mask_eq_iff_shiftr_0 pageBits_def mask_zero) apply (clarsimp simp: aag_cap_auth_def pas_refined_refl) apply (drule_tac x=frame in bspec) apply (simp add: is_aligned_no_overflow) apply (clarsimp simp: pas_refined_refl cap_links_asid_slot_def
                         label_owns_asid_slot_def cap_links_irq_def) apply (fastforce dest: cte_wp_at_valid_objs_valid_cap simp: valid_cap_def cap_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and K (authorised_asid_control_inv aag aci)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)\<rbrace> case aci of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
assert (base && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of base \<mapsto> frame));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case aci of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
assert (base && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of base \<mapsto> frame));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 x3 x4 pcap. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?P'47 x1 x2 x3 x4 () pcap ()\<rbrace> retype_region x1 (Suc 0) 0 (ArchObject ASIDPoolObj) False \<lbrace>\<lambda>rv s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> \<not> cte_wp_at is_transferable_cap x3 s \<and> is_subject aag (fst x2) \<and> is_subject aag (fst x3) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x1 x4)) \<and> is_subject aag x1 \<and> (\<forall>asid. asid_high_bits_of asid = asid_high_bits_of x4 \<longrightarrow> is_subject_asid aag asid)\<rbrace>
 2. \<And>x1 x2 x3 x4 x pcap. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?B16 x1 x2 x3 x4 x pcap\<rbrace> set_cap (max_free_index_update pcap) x3 \<lbrace>\<lambda>xa s. x4 && mask local.asid_low_bits = 0 \<longrightarrow> ?P'47 x1 x2 x3 x4 x pcap xa s\<rbrace>
 3. \<And>x1 x2 x3 x4 x. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?B14 x1 x2 x3 x4 x\<rbrace> get_cap x3 \<lbrace>?B16 x1 x2 x3 x4 x\<rbrace>
 4. \<And>x1 x2 x3 x4. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?R12 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>?B14 x1 x2 x3 x4\<rbrace>
 5. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?R12 x xa xb xc s proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 x3 x4 pcap. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?P82 x1 x2 x3 x4 () pcap ()\<rbrace> retype_region x1 (Suc 0) 0 (ArchObject ASIDPoolObj) False \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cap. \<not> is_transferable_cap cap) x3\<rbrace>
 2. \<And>x1 x2 x3 x4 pcap. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?P'81 x1 x2 x3 x4 () pcap ()\<rbrace> retype_region x1 (Suc 0) 0 (ArchObject ASIDPoolObj) False \<lbrace>\<lambda>rv s. is_subject aag (fst x2) \<and> is_subject aag (fst x3) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x1 x4)) \<and> is_subject aag x1 \<and> (\<forall>asid. asid_high_bits_of asid = asid_high_bits_of x4 \<longrightarrow> is_subject_asid aag asid)\<rbrace>
 3. \<And>x1 x2 x3 x4 x pcap. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?B16 x1 x2 x3 x4 x pcap\<rbrace> set_cap (max_free_index_update pcap) x3 \<lbrace>\<lambda>xa s. x4 && mask local.asid_low_bits = 0 \<longrightarrow> (pas_refined aag and pas_cur_domain aag and invs and caps_overlap_reserved {x1..x1 + word_of_nat (Suc 0) * 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} and (\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap False (x1 && ~~ mask pageBits) pageBits idx) (?slot63 x1 x2 x3 x4 x pcap xa) s \<and> (idx \<le> unat (x1 && mask pageBits) \<or> descendants_range_in {x1..(x1 && ~~ mask pageBits) + 2 ^ pageBits - 1} (?slot62 x1 x2 x3 x4 x pcap xa) s \<and> pspace_no_overlap (up_aligned_area x1 pageBits) s)) and K (pageBits < word_bits) and K (range_cover x1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0)) and K (\<forall>x\<in>set (retype_addrs x1 (ArchObject ASIDPoolObj) (Suc 0) 0). is_subject aag x) and K (ArchObject ASIDPoolObj = CapTableObject \<longrightarrow> 0 < 0)) s \<and> (invs and pspace_no_overlap (up_aligned_area x1 pageBits) and caps_no_overlap x1 pageBits and caps_overlap_reserved {x1..x1 + word_of_nat (Suc 0) * 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} and region_in_kernel_window {x1..(x1 && ~~ mask pageBits) + 2 ^ pageBits - 1} and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area x1 pageBits \<subseteq> cap_range c \<and> cap_is_device c = False) slot s) and K (ArchObject ASIDPoolObj = CapTableObject \<longrightarrow> 0 < 0) and K (range_cover x1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0))) s \<and> (invs and pspace_no_overlap (up_aligned_area x1 pageBits) and caps_no_overlap x1 pageBits and caps_overlap_reserved {x1..x1 + word_of_nat (Suc 0) * 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} and region_in_kernel_window {x1..(x1 && ~~ mask pageBits) + 2 ^ pageBits - 1} and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area x1 pageBits \<subseteq> cap_range c \<and> cap_is_device c = False) slot s) and K (ArchObject ASIDPoolObj = CapTableObject \<longrightarrow> 0 < 0) and K (range_cover x1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0))) s \<and> (invs and pspace_no_overlap (up_aligned_area x1 pageBits) and caps_no_overlap x1 pageBits and caps_overlap_reserved {x1..x1 + word_of_nat (Suc 0) * 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} and region_in_kernel_window {x1..(x1 && ~~ mask pageBits) + 2 ^ pageBits - 1} and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area x1 pageBits \<subseteq> cap_range c \<and> cap_is_device c = False) slot s) and K (ArchObject ASIDPoolObj = CapTableObject \<longrightarrow> 0 < 0) and K (range_cover x1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0))) s \<and> (invs and pspace_no_overlap (up_aligned_area x1 pageBits) and caps_no_overlap x1 pageBits and caps_overlap_reserved {x1..x1 + word_of_nat (Suc 0) * 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} and region_in_kernel_window {x1..(x1 && ~~ mask pageBits) + 2 ^ pageBits - 1} and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area x1 pageBits \<subseteq> cap_range c \<and> cap_is_device c = False) slot s) and K (ArchObject ASIDPoolObj = CapTableObject \<longrightarrow> 0 < 0) and K (range_cover x1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0))) s \<and> ?P82 x1 x2 x3 x4 x pcap xa s \<and> ?P'81 x1 x2 x3 x4 x pcap xa s\<rbrace>
 4. \<And>x1 x2 x3 x4 x. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?B14 x1 x2 x3 x4 x\<rbrace> get_cap x3 \<lbrace>?B16 x1 x2 x3 x4 x\<rbrace>
 5. \<And>x1 x2 x3 x4. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?R12 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>?B14 x1 x2 x3 x4\<rbrace>
 6. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?R12 x xa xb xc s
flex-flex pairs:
\<lambda>x1 x2 x3 x4 pcap. ?slot63 x1 x2 x3 x4 () pcap () \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 pcap. ?slot62 x1 x2 x3 x4 () pcap () proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 cap. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?P316 x1 x2 x3 x4 cap\<rbrace> delete_objects x1 page_bits \<lbrace>\<lambda>rv s. cte_wp_at ((=) cap) x3 s \<longrightarrow> x4 && mask local.asid_low_bits = 0 \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) x3 s \<and> aag_cap_auth aag (pasObjectAbs aag (fst x3)) cap \<and> pas_cur_domain aag s \<and> descendants_range_in (untyped_range cap) x3 s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> invs s \<and> {x1..x1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {x1..x1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} x3 s \<and> is_untyped_cap cap \<and> (\<exists>x. max_free_index_update cap = UntypedCap False (x1 && ~~ mask pageBits) pageBits x \<and> cte_wp_at (\<lambda>_. True) x3 s \<and> (x \<le> unat (x1 && mask pageBits) \<or> cte_wp_at (\<lambda>c. cap_range c = cap_range cap) x3 s \<and> descendants_range_in {x1..(x1 && ~~ mask pageBits) + 2 ^ pageBits - 1} x3 s \<and> pspace_no_overlap (up_aligned_area x1 pageBits) s)) \<and> range_cover x1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> (\<forall>x\<in>set (retype_addrs x1 (ArchObject ASIDPoolObj) (Suc 0) 0). is_subject aag x) \<and> descendants_range_in (untyped_range cap) x3 s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area x1 pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) x3 s \<and> caps_no_overlap x1 pageBits s \<and> invs s \<and> {x1..x1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {x1..x1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} x3 s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{x1..(x1 && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = x3 \<longrightarrow> up_aligned_area x1 pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> x3 \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area x1 pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) x3 s \<and> range_cover x1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) x3 s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area x1 pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) x3 s \<and> caps_no_overlap x1 pageBits s \<and> invs s \<and> {x1..x1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {x1..x1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} x3 s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{x1..(x1 && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = x3 \<longrightarrow> up_aligned_area x1 pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> x3 \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area x1 pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) x3 s \<and> range_cover x1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) x3 s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area x1 pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) x3 s \<and> caps_no_overlap x1 pageBits s \<and> invs s \<and> {x1..x1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {x1..x1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} x3 s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{x1..(x1 && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = x3 \<longrightarrow> up_aligned_area x1 pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> x3 \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area x1 pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) x3 s \<and> range_cover x1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) x3 s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area x1 pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) x3 s \<and> caps_no_overlap x1 pageBits s \<and> invs s \<and> {x1..x1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {x1..x1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} x3 s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{x1..(x1 && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = x3 \<longrightarrow> up_aligned_area x1 pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> x3 \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area x1 pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) x3 s \<and> range_cover x1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pspace_no_overlap (up_aligned_area x1 pageBits) s \<and> \<not> is_transferable_cap cap \<and> cte_wp_at (\<lambda>_. True) x3 s \<and> valid_pspace s \<and> free_index_of cap \<le> max_free_index (untyped_sz_bits cap) \<and> is_untyped_cap cap \<and> max_free_index (untyped_sz_bits cap) \<le> 2 ^ cap_bits cap \<and> range_cover x1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst x2) \<and> is_subject aag (fst x3) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x1 x4)) \<and> is_subject aag x1 \<and> (\<forall>asid. asid_high_bits_of asid = asid_high_bits_of x4 \<longrightarrow> is_subject_asid aag asid)\<rbrace>
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P316 x xa xb xc xd s) proof (prove)
goal (2 subgoals):
 1. \<And>frame slot parent base cap. aci = MakePool frame slot parent base \<Longrightarrow> \<lbrace>?P316 frame slot parent base cap\<rbrace> delete_objects frame page_bits \<lbrace>\<lambda>rv s. cte_wp_at ((=) cap) parent s \<longrightarrow> base && mask local.asid_low_bits = 0 \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) parent s \<and> aag_cap_auth aag (pasObjectAbs aag (fst parent)) cap \<and> pas_cur_domain aag s \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<exists>x. max_free_index_update cap = UntypedCap False (frame && ~~ mask pageBits) pageBits x \<and> cte_wp_at (\<lambda>_. True) parent s \<and> (x \<le> unat (frame && mask pageBits) \<or> cte_wp_at (\<lambda>c. cap_range c = cap_range cap) parent s \<and> descendants_range_in {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} parent s \<and> pspace_no_overlap (up_aligned_area frame pageBits) s)) \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> (\<forall>x\<in>set (retype_addrs frame (ArchObject ASIDPoolObj) (Suc 0) 0). is_subject aag x) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> \<not> is_transferable_cap cap \<and> cte_wp_at (\<lambda>_. True) parent s \<and> valid_pspace s \<and> free_index_of cap \<le> max_free_index (untyped_sz_bits cap) \<and> is_untyped_cap cap \<and> max_free_index (untyped_sz_bits cap) \<le> 2 ^ cap_bits cap \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst slot) \<and> is_subject aag (fst parent) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame \<and> (\<forall>asid. asid_high_bits_of asid = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid)\<rbrace>
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P316 x xa xb xc xd s) proof (prove)
goal (2 subgoals):
 1. \<And>frame slot parent base cap slot_ptr slot_idx. \<lbrakk>aci = MakePool frame slot parent base; slot = (slot_ptr, slot_idx)\<rbrakk> \<Longrightarrow> \<lbrace>?P316 frame slot parent base cap\<rbrace> delete_objects frame page_bits \<lbrace>\<lambda>rv s. cte_wp_at ((=) cap) parent s \<longrightarrow> base && mask local.asid_low_bits = 0 \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) parent s \<and> aag_cap_auth aag (pasObjectAbs aag (fst parent)) cap \<and> pas_cur_domain aag s \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<exists>x. max_free_index_update cap = UntypedCap False (frame && ~~ mask pageBits) pageBits x \<and> cte_wp_at (\<lambda>_. True) parent s \<and> (x \<le> unat (frame && mask pageBits) \<or> cte_wp_at (\<lambda>c. cap_range c = cap_range cap) parent s \<and> descendants_range_in {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} parent s \<and> pspace_no_overlap (up_aligned_area frame pageBits) s)) \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> (\<forall>x\<in>set (retype_addrs frame (ArchObject ASIDPoolObj) (Suc 0) 0). is_subject aag x) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> \<not> is_transferable_cap cap \<and> cte_wp_at (\<lambda>_. True) parent s \<and> valid_pspace s \<and> free_index_of cap \<le> max_free_index (untyped_sz_bits cap) \<and> is_untyped_cap cap \<and> max_free_index (untyped_sz_bits cap) \<le> 2 ^ cap_bits cap \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst slot) \<and> is_subject aag (fst parent) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame \<and> (\<forall>asid. asid_high_bits_of asid = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid)\<rbrace>
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P316 x xa xb xc xd s) proof (prove)
goal (2 subgoals):
 1. \<And>frame slot parent base cap slot_ptr slot_idx parent_ptr parent_idx. \<lbrakk>aci = MakePool frame slot parent base; slot = (slot_ptr, slot_idx); parent = (parent_ptr, parent_idx)\<rbrakk> \<Longrightarrow> \<lbrace>?P316 frame slot parent base cap\<rbrace> delete_objects frame page_bits \<lbrace>\<lambda>rv s. cte_wp_at ((=) cap) parent s \<longrightarrow> base && mask local.asid_low_bits = 0 \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) parent s \<and> aag_cap_auth aag (pasObjectAbs aag (fst parent)) cap \<and> pas_cur_domain aag s \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<exists>x. max_free_index_update cap = UntypedCap False (frame && ~~ mask pageBits) pageBits x \<and> cte_wp_at (\<lambda>_. True) parent s \<and> (x \<le> unat (frame && mask pageBits) \<or> cte_wp_at (\<lambda>c. cap_range c = cap_range cap) parent s \<and> descendants_range_in {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} parent s \<and> pspace_no_overlap (up_aligned_area frame pageBits) s)) \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> (\<forall>x\<in>set (retype_addrs frame (ArchObject ASIDPoolObj) (Suc 0) 0). is_subject aag x) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> \<not> is_transferable_cap cap \<and> cte_wp_at (\<lambda>_. True) parent s \<and> valid_pspace s \<and> free_index_of cap \<le> max_free_index (untyped_sz_bits cap) \<and> is_untyped_cap cap \<and> max_free_index (untyped_sz_bits cap) \<le> 2 ^ cap_bits cap \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst slot) \<and> is_subject aag (fst parent) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame \<and> (\<forall>asid. asid_high_bits_of asid = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid)\<rbrace>
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P316 x xa xb xc xd s) proof (prove)
goal (3 subgoals):
 1. \<And>frame slot parent base cap slot_ptr slot_idx parent_ptr parent_idx. \<lbrakk>aci = MakePool frame slot parent base; slot = (slot_ptr, slot_idx); parent = (parent_ptr, parent_idx)\<rbrakk> \<Longrightarrow> \<lbrace>?P316 frame slot parent base cap\<rbrace> delete_objects frame page_bits \<lbrace>\<lambda>rv s. (\<exists>idx. cte_wp_at ((=) (UntypedCap False frame pageBits idx)) parent s) \<and> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> invs s \<and> descendants_range_in {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag slot_ptr \<and> is_subject aag parent_ptr \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x)\<rbrace>
 2. \<And>frame slot parent base cap slot_ptr slot_idx parent_ptr parent_idx rv s. \<lbrakk>aci = MakePool frame slot parent base; slot = (slot_ptr, slot_idx); parent = (parent_ptr, parent_idx); (\<exists>idx. cte_wp_at ((=) (UntypedCap False frame pageBits idx)) parent s) \<and> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> invs s \<and> descendants_range_in {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag slot_ptr \<and> is_subject aag parent_ptr \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) parent s \<longrightarrow> base && mask local.asid_low_bits = 0 \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) parent s \<and> aag_cap_auth aag (pasObjectAbs aag (fst parent)) cap \<and> pas_cur_domain aag s \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<exists>x. max_free_index_update cap = UntypedCap False (frame && ~~ mask pageBits) pageBits x \<and> cte_wp_at (\<lambda>_. True) parent s \<and> (x \<le> unat (frame && mask pageBits) \<or> cte_wp_at (\<lambda>c. cap_range c = cap_range cap) parent s \<and> descendants_range_in {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} parent s \<and> pspace_no_overlap (up_aligned_area frame pageBits) s)) \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> (\<forall>x\<in>set (retype_addrs frame (ArchObject ASIDPoolObj) (Suc 0) 0). is_subject aag x) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> \<not> is_transferable_cap cap \<and> cte_wp_at (\<lambda>_. True) parent s \<and> valid_pspace s \<and> free_index_of cap \<le> max_free_index (untyped_sz_bits cap) \<and> is_untyped_cap cap \<and> max_free_index (untyped_sz_bits cap) \<le> 2 ^ cap_bits cap \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst slot) \<and> is_subject aag (fst parent) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame \<and> (\<forall>asid. asid_high_bits_of asid = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid)
 3. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P316 x xa xb xc xd s) proof (prove)
goal (3 subgoals):
 1. \<And>frame slot parent base cap slot_ptr slot_idx parent_ptr parent_idx. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; slot = (slot_ptr, slot_idx); parent = (parent_ptr, parent_idx)\<rbrakk> \<Longrightarrow> \<lbrace>?P316 frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base cap\<rbrace> delete_objects frame pageBits \<lbrace>\<lambda>rv s. (\<exists>idx. cte_wp_at ((=) (UntypedCap False frame pageBits idx)) (parent_ptr, parent_idx) s) \<and> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> invs s \<and> descendants_range_in {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag slot_ptr \<and> is_subject aag parent_ptr \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x)\<rbrace>
 2. \<And>frame slot parent base cap slot_ptr slot_idx parent_ptr parent_idx rv s. \<lbrakk>aci = MakePool frame slot parent base; slot = (slot_ptr, slot_idx); parent = (parent_ptr, parent_idx); (\<exists>idx. cte_wp_at ((=) (UntypedCap False frame pageBits idx)) parent s) \<and> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> invs s \<and> descendants_range_in {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag slot_ptr \<and> is_subject aag parent_ptr \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) parent s \<longrightarrow> base && mask local.asid_low_bits = 0 \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) parent s \<and> aag_cap_auth aag (pasObjectAbs aag (fst parent)) cap \<and> pas_cur_domain aag s \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<exists>x. max_free_index_update cap = UntypedCap False (frame && ~~ mask pageBits) pageBits x \<and> cte_wp_at (\<lambda>_. True) parent s \<and> (x \<le> unat (frame && mask pageBits) \<or> cte_wp_at (\<lambda>c. cap_range c = cap_range cap) parent s \<and> descendants_range_in {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} parent s \<and> pspace_no_overlap (up_aligned_area frame pageBits) s)) \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> (\<forall>x\<in>set (retype_addrs frame (ArchObject ASIDPoolObj) (Suc 0) 0). is_subject aag x) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) parent s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) parent s \<and> caps_no_overlap frame pageBits s \<and> invs s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} parent s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. ((x, xa) = parent \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x, xa) \<noteq> parent \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> \<not> is_transferable_cap cap \<and> cte_wp_at (\<lambda>_. True) parent s \<and> valid_pspace s \<and> free_index_of cap \<le> max_free_index (untyped_sz_bits cap) \<and> is_untyped_cap cap \<and> max_free_index (untyped_sz_bits cap) \<le> 2 ^ cap_bits cap \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst slot) \<and> is_subject aag (fst parent) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame \<and> (\<forall>asid. asid_high_bits_of asid = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid)
 3. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P316 x xa xb xc xd s) proof (prove)
goal (2 subgoals):
 1. \<And>frame slot parent base cap slot_ptr slot_idx parent_ptr parent_idx s. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; slot = (slot_ptr, slot_idx); parent = (parent_ptr, parent_idx); (\<exists>idx. cte_wp_at ((=) (UntypedCap False frame pageBits idx)) (parent_ptr, parent_idx) s) \<and> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> pspace_no_overlap (up_aligned_area frame pageBits) s \<and> invs s \<and> descendants_range_in {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag slot_ptr \<and> is_subject aag parent_ptr \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (parent_ptr, parent_idx) s \<longrightarrow> base && mask local.asid_low_bits = 0 \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (parent_ptr, parent_idx) s \<and> pas_cap_cur_auth aag cap \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<exists>x. max_free_index_update cap = UntypedCap False (frame && ~~ mask pageBits) pageBits x \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> (x \<le> unat (frame && mask pageBits) \<or> cte_wp_at (\<lambda>c. cap_range c = cap_range cap) (parent_ptr, parent_idx) s)) \<and> (\<forall>x\<in>set (retype_addrs frame (ArchObject ASIDPoolObj) (Suc 0) 0). is_subject aag x) \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> \<not> is_transferable_cap cap \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> valid_pspace s \<and> free_index_of cap \<le> max_free_index (untyped_sz_bits cap) \<and> is_untyped_cap cap \<and> max_free_index (untyped_sz_bits cap) \<le> 2 ^ cap_bits cap
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. (\<exists>xa. cte_wp_at ((=) (UntypedCap False x pageBits xa)) xb s \<and> fst xb \<notin> {x..x + 2 ^ pageBits - 1}) \<and> (\<forall>x\<in>ptr_range x pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> (pspace_aligned and valid_objs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev437 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) (?slot435 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) s)) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev x pageBits f)) slot s \<and> descendants_range (UntypedCap dev x pageBits f) slot s)) s \<and> (invs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev452 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) xb s) and descendants_range_in {x..x + 2 ^ pageBits - 1} xb) s \<and> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst xa) \<and> is_subject aag (fst xb) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x xc)) \<and> is_subject aag x \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of xc \<longrightarrow> is_subject_asid aag x)) proof (prove)
goal (2 subgoals):
 1. \<And>frame base cap slot_ptr slot_idx parent_ptr parent_idx s idx. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at ((=) (UntypedCap False frame pageBits idx)) (parent_ptr, parent_idx) s; \<forall>x\<in>ptr_range frame pageBits. is_subject aag x; pas_refined aag s; pas_cur_domain aag s; pspace_no_overlap (up_aligned_area frame pageBits) s; invs s; descendants_range_in {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s; range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0); is_subject aag slot_ptr; is_subject aag parent_ptr; pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)); is_subject aag frame; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x; cte_wp_at ((=) cap) (parent_ptr, parent_idx) s; base && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (parent_ptr, parent_idx) s \<and> pas_cap_cur_auth aag cap \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<exists>x. max_free_index_update cap = UntypedCap False (frame && ~~ mask pageBits) pageBits x \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> (x \<le> unat (frame && mask pageBits) \<or> cte_wp_at (\<lambda>c. cap_range c = cap_range cap) (parent_ptr, parent_idx) s)) \<and> (\<forall>x\<in>set (retype_addrs frame (ArchObject ASIDPoolObj) (Suc 0) 0). is_subject aag x) \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> \<not> is_transferable_cap cap \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> valid_pspace s \<and> free_index_of cap \<le> max_free_index (untyped_sz_bits cap) \<and> is_untyped_cap cap \<and> max_free_index (untyped_sz_bits cap) \<le> 2 ^ cap_bits cap
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. (\<exists>xa. cte_wp_at ((=) (UntypedCap False x pageBits xa)) xb s \<and> fst xb \<notin> {x..x + 2 ^ pageBits - 1}) \<and> (\<forall>x\<in>ptr_range x pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> (pspace_aligned and valid_objs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev437 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) (?slot435 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) s)) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev x pageBits f)) slot s \<and> descendants_range (UntypedCap dev x pageBits f) slot s)) s \<and> (invs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev452 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) xb s) and descendants_range_in {x..x + 2 ^ pageBits - 1} xb) s \<and> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst xa) \<and> is_subject aag (fst xb) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x xc)) \<and> is_subject aag x \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of xc \<longrightarrow> is_subject_asid aag x)) proof (prove)
goal (2 subgoals):
 1. \<And>frame base cap slot_ptr slot_idx parent_ptr parent_idx s idx. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at ((=) (UntypedCap False frame pageBits idx)) (parent_ptr, parent_idx) s; \<forall>x\<in>ptr_range frame pageBits. is_subject aag x; pas_refined aag s; pas_cur_domain aag s; pspace_no_overlap (up_aligned_area frame pageBits) s; invs s; descendants_range_in {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s; range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0); is_subject aag slot_ptr; is_subject aag parent_ptr; pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)); is_subject aag frame; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x; cte_wp_at ((=) cap) (parent_ptr, parent_idx) s; base && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (parent_ptr, parent_idx) s \<and> pas_cap_cur_auth aag cap \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<exists>x. max_free_index_update cap = UntypedCap False (frame && ~~ mask pageBits) pageBits x \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> (x \<le> unat (frame && mask pageBits) \<or> cte_wp_at (\<lambda>c. cap_range c = cap_range cap) (parent_ptr, parent_idx) s)) \<and> (\<forall>x\<in>set (retype_addrs frame (ArchObject ASIDPoolObj) (Suc 0) 0). is_subject aag x) \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> \<not> is_transferable_cap cap \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> valid_pspace s \<and> free_index_of cap \<le> max_free_index (untyped_sz_bits cap) \<and> is_untyped_cap cap \<and> max_free_index (untyped_sz_bits cap) \<le> 2 ^ cap_bits cap
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. (\<exists>xa. cte_wp_at ((=) (UntypedCap False x pageBits xa)) xb s \<and> fst xb \<notin> {x..x + 2 ^ pageBits - 1}) \<and> (\<forall>x\<in>ptr_range x pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> (pspace_aligned and valid_objs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev437 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) (?slot435 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) s)) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev x pageBits f)) slot s \<and> descendants_range (UntypedCap dev x pageBits f) slot s)) s \<and> (invs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev452 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) xb s) and descendants_range_in {x..x + 2 ^ pageBits - 1} xb) s \<and> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst xa) \<and> is_subject aag (fst xb) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x xc)) \<and> is_subject aag x \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of xc \<longrightarrow> is_subject_asid aag x)) proof (prove)
goal (2 subgoals):
 1. \<And>frame base cap slot_ptr slot_idx parent_ptr parent_idx s idx. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at ((=) (UntypedCap False frame pageBits idx)) (parent_ptr, parent_idx) s; \<forall>x\<in>ptr_range frame pageBits. is_subject aag x; pas_refined aag s; pas_cur_domain aag s; pspace_no_overlap (up_aligned_area frame pageBits) s; invs s; descendants_range_in {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s; range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0); is_subject aag slot_ptr; is_subject aag parent_ptr; pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)); is_subject aag frame; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x; cte_wp_at ((=) cap) (parent_ptr, parent_idx) s; base && mask local.asid_low_bits = 0; is_aligned frame pageBits\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (parent_ptr, parent_idx) s \<and> pas_cap_cur_auth aag cap \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<exists>x. max_free_index_update cap = UntypedCap False (frame && ~~ mask pageBits) pageBits x \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> (x \<le> unat (frame && mask pageBits) \<or> cte_wp_at (\<lambda>c. cap_range c = cap_range cap) (parent_ptr, parent_idx) s)) \<and> (\<forall>x\<in>set (retype_addrs frame (ArchObject ASIDPoolObj) (Suc 0) 0). is_subject aag x) \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> descendants_range_in (untyped_range cap) (parent_ptr, parent_idx) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (parent_ptr, parent_idx) s \<and> caps_no_overlap frame pageBits s \<and> {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {frame..frame + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (parent_ptr, parent_idx) s \<and> is_untyped_cap cap \<and> (\<forall>x\<in>{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> up_aligned_area frame pageBits \<subseteq> cap_range cap \<and> \<not> cap_is_device (max_free_index_update cap)) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> cte_wp_at (\<lambda>a. up_aligned_area frame pageBits \<subseteq> cap_range a \<and> \<not> cap_is_device a) (x, xa) s)) \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> \<not> is_transferable_cap cap \<and> cte_wp_at (\<lambda>_. True) (parent_ptr, parent_idx) s \<and> valid_pspace s \<and> free_index_of cap \<le> max_free_index (untyped_sz_bits cap) \<and> is_untyped_cap cap \<and> max_free_index (untyped_sz_bits cap) \<le> 2 ^ cap_bits cap
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. (\<exists>xa. cte_wp_at ((=) (UntypedCap False x pageBits xa)) xb s \<and> fst xb \<notin> {x..x + 2 ^ pageBits - 1}) \<and> (\<forall>x\<in>ptr_range x pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> (pspace_aligned and valid_objs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev437 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) (?slot435 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) s)) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev x pageBits f)) slot s \<and> descendants_range (UntypedCap dev x pageBits f) slot s)) s \<and> (invs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev452 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) xb s) and descendants_range_in {x..x + 2 ^ pageBits - 1} xb) s \<and> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst xa) \<and> is_subject aag (fst xb) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x xc)) \<and> is_subject aag x \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of xc \<longrightarrow> is_subject_asid aag x)) proof (prove)
goal (2 subgoals):
 1. \<And>frame base slot_ptr slot_idx parent_ptr parent_idx s idx. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; fst (get_cap (parent_ptr, parent_idx) s) = {(UntypedCap False frame pageBits idx, s)}; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; pas_refined aag s; pas_cur_domain aag s; pspace_no_overlap {frame..frame + (2 ^ pageBits - 1)} s; invs s; descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s; range_cover frame pageBits pageBits (Suc 0); is_subject aag slot_ptr; is_subject aag parent_ptr; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<and> x \<noteq> 0 \<longrightarrow> label_owns_asid_slot aag (pasSubject aag) x; is_subject aag frame; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x; base && mask local.asid_low_bits = 0; is_aligned frame pageBits\<rbrakk> \<Longrightarrow> caps_no_overlap frame pageBits s \<and> (\<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> frame \<le> frame + (2 ^ pageBits - 1) \<longrightarrow> frame + (2 ^ pageBits - 1) \<le> frame + 2 ^ pageBits - 1) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> (\<exists>cap. fst (get_cap (x, xa) s) = {(cap, s)} \<and> {frame..frame + (2 ^ pageBits - 1)} \<subseteq> cap_range cap \<and> \<not> cap_is_device cap))) \<and> free_index_of (UntypedCap False frame pageBits idx) \<le> max_free_index pageBits \<and> max_free_index pageBits \<le> 2 ^ pageBits
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. (\<exists>xa. cte_wp_at ((=) (UntypedCap False x pageBits xa)) xb s \<and> fst xb \<notin> {x..x + 2 ^ pageBits - 1}) \<and> (\<forall>x\<in>ptr_range x pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> (pspace_aligned and valid_objs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev437 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) (?slot435 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) s)) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev x pageBits f)) slot s \<and> descendants_range (UntypedCap dev x pageBits f) slot s)) s \<and> (invs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev452 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) xb s) and descendants_range_in {x..x + 2 ^ pageBits - 1} xb) s \<and> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst xa) \<and> is_subject aag (fst xb) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x xc)) \<and> is_subject aag x \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of xc \<longrightarrow> is_subject_asid aag x)) proof (prove)
goal (2 subgoals):
 1. \<And>frame base slot_ptr slot_idx parent_ptr parent_idx s idx. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; fst (get_cap (parent_ptr, parent_idx) s) = {(UntypedCap False frame pageBits idx, s)}; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; pas_refined aag s; pas_cur_domain aag s; pspace_no_overlap {frame..frame + (2 ^ pageBits - 1)} s; invs s; descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s; range_cover frame pageBits pageBits (Suc 0); is_subject aag slot_ptr; is_subject aag parent_ptr; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<and> x \<noteq> 0 \<longrightarrow> label_owns_asid_slot aag (pasSubject aag) x; is_subject aag frame; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x; base && mask local.asid_low_bits = 0; is_aligned frame pageBits\<rbrakk> \<Longrightarrow> (\<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) \<and> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> frame \<le> frame + (2 ^ pageBits - 1) \<longrightarrow> frame + (2 ^ pageBits - 1) \<le> frame + 2 ^ pageBits - 1) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> (\<exists>cap. fst (get_cap (x, xa) s) = {(cap, s)} \<and> {frame..frame + (2 ^ pageBits - 1)} \<subseteq> cap_range cap \<and> \<not> cap_is_device cap))) \<and> free_index_of (UntypedCap False frame pageBits idx) \<le> max_free_index pageBits \<and> max_free_index pageBits \<le> 2 ^ pageBits
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. (\<exists>xa. cte_wp_at ((=) (UntypedCap False x pageBits xa)) xb s \<and> fst xb \<notin> {x..x + 2 ^ pageBits - 1}) \<and> (\<forall>x\<in>ptr_range x pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> (pspace_aligned and valid_objs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev437 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) (?slot435 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) s)) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev x pageBits f)) slot s \<and> descendants_range (UntypedCap dev x pageBits f) slot s)) s \<and> (invs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev452 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) xb s) and descendants_range_in {x..x + 2 ^ pageBits - 1} xb) s \<and> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst xa) \<and> is_subject aag (fst xb) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x xc)) \<and> is_subject aag x \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of xc \<longrightarrow> is_subject_asid aag x)) proof (prove)
goal (3 subgoals):
 1. \<And>frame base slot_ptr slot_idx parent_ptr parent_idx s idx. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; fst (get_cap (parent_ptr, parent_idx) s) = {(UntypedCap False frame pageBits idx, s)}; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; pas_refined aag s; pas_cur_domain aag s; pspace_no_overlap {frame..frame + (2 ^ pageBits - 1)} s; invs s; descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s; range_cover frame pageBits pageBits (Suc 0); is_subject aag slot_ptr; is_subject aag parent_ptr; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<and> x \<noteq> 0 \<longrightarrow> label_owns_asid_slot aag (pasSubject aag) x; is_subject aag frame; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x; base && mask local.asid_low_bits = 0; is_aligned frame pageBits\<rbrakk> \<Longrightarrow> \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow
 2. \<And>frame base slot_ptr slot_idx parent_ptr parent_idx s idx. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; fst (get_cap (parent_ptr, parent_idx) s) = {(UntypedCap False frame pageBits idx, s)}; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; pas_refined aag s; pas_cur_domain aag s; pspace_no_overlap {frame..frame + (2 ^ pageBits - 1)} s; invs s; descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s; range_cover frame pageBits pageBits (Suc 0); is_subject aag slot_ptr; is_subject aag parent_ptr; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<and> x \<noteq> 0 \<longrightarrow> label_owns_asid_slot aag (pasSubject aag) x; is_subject aag frame; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x; base && mask local.asid_low_bits = 0; is_aligned frame pageBits\<rbrakk> \<Longrightarrow> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> frame \<le> frame + (2 ^ pageBits - 1) \<longrightarrow> frame + (2 ^ pageBits - 1) \<le> frame + 2 ^ pageBits - 1) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> (\<exists>cap. fst (get_cap (x, xa) s) = {(cap, s)} \<and> {frame..frame + (2 ^ pageBits - 1)} \<subseteq> cap_range cap \<and> \<not> cap_is_device cap))) \<and> free_index_of (UntypedCap False frame pageBits idx) \<le> max_free_index pageBits \<and> max_free_index pageBits \<le> 2 ^ pageBits
 3. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. (\<exists>xa. cte_wp_at ((=) (UntypedCap False x pageBits xa)) xb s \<and> fst xb \<notin> {x..x + 2 ^ pageBits - 1}) \<and> (\<forall>x\<in>ptr_range x pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> (pspace_aligned and valid_objs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev437 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) (?slot435 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) s)) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev x pageBits f)) slot s \<and> descendants_range (UntypedCap dev x pageBits f) slot s)) s \<and> (invs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev452 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) xb s) and descendants_range_in {x..x + 2 ^ pageBits - 1} xb) s \<and> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst xa) \<and> is_subject aag (fst xb) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x xc)) \<and> is_subject aag x \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of xc \<longrightarrow> is_subject_asid aag x)) proof (prove)
goal (5 subgoals):
 1. \<And>frame base slot_ptr slot_idx parent_ptr parent_idx s idx. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; fst (get_cap (parent_ptr, parent_idx) s) = {(UntypedCap False frame pageBits idx, s)}; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; pas_refined aag s; pas_cur_domain aag s; pspace_no_overlap {frame..frame + (2 ^ pageBits - 1)} s; invs s; descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s; range_cover frame pageBits pageBits (Suc 0); is_subject aag slot_ptr; is_subject aag parent_ptr; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<and> x \<noteq> 0 \<longrightarrow> label_owns_asid_slot aag (pasSubject aag) x; is_subject aag frame; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x; base && mask local.asid_low_bits = 0; is_aligned frame pageBits\<rbrakk> \<Longrightarrow> caps_of_state s (parent_ptr, parent_idx) = Some (?cap502 frame base slot_ptr slot_idx parent_ptr parent_idx s idx)
 2. \<And>frame base slot_ptr slot_idx parent_ptr parent_idx s idx. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; fst (get_cap (parent_ptr, parent_idx) s) = {(UntypedCap False frame pageBits idx, s)}; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; pas_refined aag s; pas_cur_domain aag s; pspace_no_overlap {frame..frame + (2 ^ pageBits - 1)} s; invs s; descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s; range_cover frame pageBits pageBits (Suc 0); is_subject aag slot_ptr; is_subject aag parent_ptr; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<and> x \<noteq> 0 \<longrightarrow> label_owns_asid_slot aag (pasSubject aag) x; is_subject aag frame; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x; base && mask local.asid_low_bits = 0; is_aligned frame pageBits\<rbrakk> \<Longrightarrow> cap_refs_in_kernel_window s
 3. \<And>frame base slot_ptr slot_idx parent_ptr parent_idx s idx. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; fst (get_cap (parent_ptr, parent_idx) s) = {(UntypedCap False frame pageBits idx, s)}; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; pas_refined aag s; pas_cur_domain aag s; pspace_no_overlap {frame..frame + (2 ^ pageBits - 1)} s; invs s; descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s; range_cover frame pageBits pageBits (Suc 0); is_subject aag slot_ptr; is_subject aag parent_ptr; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<and> x \<noteq> 0 \<longrightarrow> label_owns_asid_slot aag (pasSubject aag) x; is_subject aag frame; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x; base && mask local.asid_low_bits = 0; is_aligned frame pageBits; \<forall>ref\<in>cap_range (?cap502 frame base slot_ptr slot_idx parent_ptr parent_idx s idx). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow
 4. \<And>frame base slot_ptr slot_idx parent_ptr parent_idx s idx. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; fst (get_cap (parent_ptr, parent_idx) s) = {(UntypedCap False frame pageBits idx, s)}; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; pas_refined aag s; pas_cur_domain aag s; pspace_no_overlap {frame..frame + (2 ^ pageBits - 1)} s; invs s; descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s; range_cover frame pageBits pageBits (Suc 0); is_subject aag slot_ptr; is_subject aag parent_ptr; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<and> x \<noteq> 0 \<longrightarrow> label_owns_asid_slot aag (pasSubject aag) x; is_subject aag frame; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x; base && mask local.asid_low_bits = 0; is_aligned frame pageBits\<rbrakk> \<Longrightarrow> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> frame \<le> frame + (2 ^ pageBits - 1) \<longrightarrow> frame + (2 ^ pageBits - 1) \<le> frame + 2 ^ pageBits - 1) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> (\<exists>cap. fst (get_cap (x, xa) s) = {(cap, s)} \<and> {frame..frame + (2 ^ pageBits - 1)} \<subseteq> cap_range cap \<and> \<not> cap_is_device cap))) \<and> free_index_of (UntypedCap False frame pageBits idx) \<le> max_free_index pageBits \<and> max_free_index pageBits \<le> 2 ^ pageBits
 5. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. (\<exists>xa. cte_wp_at ((=) (UntypedCap False x pageBits xa)) xb s \<and> fst xb \<notin> {x..x + 2 ^ pageBits - 1}) \<and> (\<forall>x\<in>ptr_range x pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> (pspace_aligned and valid_objs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev437 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) (?slot435 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) s)) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev x pageBits f)) slot s \<and> descendants_range (UntypedCap dev x pageBits f) slot s)) s \<and> (invs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev452 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) xb s) and descendants_range_in {x..x + 2 ^ pageBits - 1} xb) s \<and> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst xa) \<and> is_subject aag (fst xb) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x xc)) \<and> is_subject aag x \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of xc \<longrightarrow> is_subject_asid aag x)) proof (prove)
goal (2 subgoals):
 1. \<And>frame base slot_ptr slot_idx parent_ptr parent_idx s idx. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; fst (get_cap (parent_ptr, parent_idx) s) = {(UntypedCap False frame pageBits idx, s)}; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; pas_refined aag s; pas_cur_domain aag s; pspace_no_overlap {frame..frame + (2 ^ pageBits - 1)} s; invs s; descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s; range_cover frame pageBits pageBits (Suc 0); is_subject aag slot_ptr; is_subject aag parent_ptr; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<and> x \<noteq> 0 \<longrightarrow> label_owns_asid_slot aag (pasSubject aag) x; is_subject aag frame; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x; base && mask local.asid_low_bits = 0; is_aligned frame pageBits\<rbrakk> \<Longrightarrow> (\<exists>x xa. (x = parent_ptr \<and> xa = parent_idx \<longrightarrow> frame \<le> frame + (2 ^ pageBits - 1) \<longrightarrow> frame + (2 ^ pageBits - 1) \<le> frame + 2 ^ pageBits - 1) \<and> ((x = parent_ptr \<longrightarrow> xa \<noteq> parent_idx) \<longrightarrow> (\<exists>cap. fst (get_cap (x, xa) s) = {(cap, s)} \<and> {frame..frame + (2 ^ pageBits - 1)} \<subseteq> cap_range cap \<and> \<not> cap_is_device cap))) \<and> free_index_of (UntypedCap False frame pageBits idx) \<le> max_free_index pageBits \<and> max_free_index pageBits \<le> 2 ^ pageBits
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. (\<exists>xa. cte_wp_at ((=) (UntypedCap False x pageBits xa)) xb s \<and> fst xb \<notin> {x..x + 2 ^ pageBits - 1}) \<and> (\<forall>x\<in>ptr_range x pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> (pspace_aligned and valid_objs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev437 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) (?slot435 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) s)) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev x pageBits f)) slot s \<and> descendants_range (UntypedCap dev x pageBits f) slot s)) s \<and> (invs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev452 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) xb s) and descendants_range_in {x..x + 2 ^ pageBits - 1} xb) s \<and> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst xa) \<and> is_subject aag (fst xb) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x xc)) \<and> is_subject aag x \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of xc \<longrightarrow> is_subject_asid aag x)) proof (prove)
goal (2 subgoals):
 1. \<And>frame base slot_ptr slot_idx parent_ptr parent_idx s idx. \<lbrakk>aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; fst (get_cap (parent_ptr, parent_idx) s) = {(UntypedCap False frame pageBits idx, s)}; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; pas_refined aag s; pas_cur_domain aag s; pspace_no_overlap {frame..frame + (2 ^ pageBits - 1)} s; invs s; descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s; range_cover frame pageBits pageBits (Suc 0); is_subject aag slot_ptr; is_subject aag parent_ptr; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<and> x \<noteq> 0 \<longrightarrow> label_owns_asid_slot aag (pasSubject aag) x; is_subject aag frame; \<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> is_subject_asid aag x; base && mask local.asid_low_bits = 0; is_aligned frame pageBits\<rbrakk> \<Longrightarrow> free_index_of (UntypedCap False frame pageBits idx) \<le> max_free_index pageBits \<and> max_free_index pageBits \<le> 2 ^ pageBits
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. (\<exists>xa. cte_wp_at ((=) (UntypedCap False x pageBits xa)) xb s \<and> fst xb \<notin> {x..x + 2 ^ pageBits - 1}) \<and> (\<forall>x\<in>ptr_range x pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> (pspace_aligned and valid_objs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev437 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) (?slot435 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) s)) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev x pageBits f)) slot s \<and> descendants_range (UntypedCap dev x pageBits f) slot s)) s \<and> (invs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev452 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) xb s) and descendants_range_in {x..x + 2 ^ pageBits - 1} xb) s \<and> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst xa) \<and> is_subject aag (fst xb) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x xc)) \<and> is_subject aag x \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of xc \<longrightarrow> is_subject_asid aag x)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. (\<exists>xa. cte_wp_at ((=) (UntypedCap False x pageBits xa)) xb s \<and> fst xb \<notin> {x..x + 2 ^ pageBits - 1}) \<and> (\<forall>x\<in>ptr_range x pageBits. is_subject aag x) \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> (pspace_aligned and valid_objs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev437 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) (?slot435 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) s)) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev x pageBits f)) slot s \<and> descendants_range (UntypedCap dev x pageBits f) slot s)) s \<and> (invs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap (?dev452 x (fst xa) (snd xa) (fst xb) (snd xb) xa xb xc xd) x pageBits idx)) xb s) and descendants_range_in {x..x + 2 ^ pageBits - 1} xb) s \<and> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> is_subject aag (fst xa) \<and> is_subject aag (fst xb) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x xc)) \<and> is_subject aag x \<and> (\<forall>x. asid_high_bits_of x = asid_high_bits_of xc \<longrightarrow> is_subject_asid aag x)) proof (prove)
goal (1 subgoal):
 1. \<And>s x a b aa ba xa. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool x (a, b) (aa, ba) xa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_subject aag a; cap_table_at (length b) a s; is_aligned x pageBits; ex_cte_cap_wp_to is_cnode_cap (a, b) s; \<forall>asid. is_subject_asid aag asid; a = aa \<longrightarrow> b \<noteq> ba; is_subject aag aa; \<forall>x\<in>{x..x + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> (\<exists>xa. cte_wp_at ((=) (UntypedCap False x pageBits xa)) (aa, ba) s) \<and> (x \<le> aa \<longrightarrow> \<not> aa \<le> x + 2 ^ pageBits - 1) \<and> (\<forall>x\<in>ptr_range x pageBits. is_subject aag x) \<and> pspace_aligned s \<and> valid_objs s \<and> (\<forall>xb. (\<exists>idx. cte_wp_at ((=) (UntypedCap (?dev437 x a b aa ba (a, b) (aa, ba) xa xb) x pageBits idx)) (?slot435 x a b aa ba (a, b) (aa, ba) xa xb) s) \<and> (\<exists>a b dev f. cte_wp_at ((=) (UntypedCap dev x pageBits f)) (a, b) s \<and> descendants_range (UntypedCap dev x pageBits f) (a, b) s) \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap (?dev452 x a b aa ba (a, b) (aa, ba) xa xb) x pageBits idx)) (aa, ba) s) \<and> descendants_range_in {x..x + 2 ^ pageBits - 1} (aa, ba) s \<and> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap x xa)) \<and> is_subject aag x) proof (prove)
goal (1 subgoal):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> (\<exists>x. cte_wp_at ((=) (UntypedCap False frame pageBits x)) (parent_ptr, parent_idx) s) \<and> (frame \<le> parent_ptr \<longrightarrow> \<not> parent_ptr \<le> frame + 2 ^ pageBits - 1) \<and> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pspace_aligned s \<and> valid_objs s \<and> (\<forall>x. (\<exists>idx. cte_wp_at ((=) (UntypedCap (?dev437 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) (?slot435 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) s) \<and> (\<exists>a b dev f. cte_wp_at ((=) (UntypedCap dev frame pageBits f)) (a, b) s \<and> descendants_range (UntypedCap dev frame pageBits f) (a, b) s) \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap (?dev452 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) (parent_ptr, parent_idx) s) \<and> descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame) proof (prove)
goal (2 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits\<rbrakk> \<Longrightarrow> (\<exists>x. cte_wp_at ((=) (UntypedCap False frame pageBits x)) (parent_ptr, parent_idx) s) \<and> (frame \<le> parent_ptr \<longrightarrow> \<not> parent_ptr \<le> frame + 2 ^ pageBits - 1) \<and> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pspace_aligned s \<and> valid_objs s \<and> (\<forall>x. (\<exists>idx. cte_wp_at ((=) (UntypedCap (?dev437 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) (?slot435 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) s) \<and> (\<exists>a b dev f. cte_wp_at ((=) (UntypedCap dev frame pageBits f)) (a, b) s \<and> descendants_range (UntypedCap dev frame pageBits f) (a, b) s) \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap (?dev452 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) (parent_ptr, parent_idx) s) \<and> descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame)
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits proof (prove)
goal (2 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> (frame \<le> parent_ptr \<longrightarrow> \<not> parent_ptr \<le> frame + 2 ^ pageBits - 1) \<and> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pspace_aligned s \<and> valid_objs s \<and> (\<forall>x. (\<exists>idx. caps_of_state s (?slot435 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) = Some (UntypedCap (?dev437 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) \<and> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev frame pageBits f) \<and> descendants_range (UntypedCap dev frame pageBits f) (a, b) s) \<and> \<not> ?dev452 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x \<and> descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame)
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits proof (prove)
goal (3 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> frame \<le> parent_ptr \<longrightarrow> \<not> parent_ptr \<le> frame + 2 ^ pageBits - 1
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pspace_aligned s \<and> valid_objs s \<and> (\<forall>x. (\<exists>idx. caps_of_state s (?slot435 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) = Some (UntypedCap (?dev437 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) \<and> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev frame pageBits f) \<and> descendants_range (UntypedCap dev frame pageBits f) (a, b) s) \<and> \<not> ?dev452 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x \<and> descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame)
 3. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits proof (prove)
goal (8 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> descendants_range_in (?S708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx) (?slot708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx) s
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx)) (?slot708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx) s
 3. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> is_untyped_cap (?cap708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx)
 4. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> ?S708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx = untyped_range (?cap708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx)
 5. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> ?T708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx \<subseteq> ?S708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx
 6. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx); fst (?slot708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx) \<notin> ?T708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx\<rbrakk> \<Longrightarrow> frame \<le> parent_ptr \<longrightarrow> \<not> parent_ptr \<le> frame + 2 ^ pageBits - 1
 7. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pspace_aligned s \<and> valid_objs s \<and> (\<forall>x. (\<exists>idx. caps_of_state s (?slot435 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) = Some (UntypedCap (?dev437 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) \<and> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev frame pageBits f) \<and> descendants_range (UntypedCap dev frame pageBits f) (a, b) s) \<and> \<not> ?dev452 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x \<and> descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame)
 8. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits proof (prove)
goal (7 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx)) (parent_ptr, parent_idx) s
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> is_untyped_cap (?cap708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx)
 3. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> ?S708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx = untyped_range (?cap708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx)
 4. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> ?T708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx \<subseteq> ?S708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx
 5. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx); fst (parent_ptr, parent_idx) \<notin> ?T708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx\<rbrakk> \<Longrightarrow> frame \<le> parent_ptr \<longrightarrow> \<not> parent_ptr \<le> frame + 2 ^ pageBits - 1
 6. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pspace_aligned s \<and> valid_objs s \<and> (\<forall>x. (\<exists>idx. caps_of_state s (?slot435 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) = Some (UntypedCap (?dev437 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) \<and> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev frame pageBits f) \<and> descendants_range (UntypedCap dev frame pageBits f) (a, b) s) \<and> \<not> ?dev452 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x \<and> descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame)
 7. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits proof (prove)
goal (6 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> is_untyped_cap (UntypedCap False frame pageBits idx)
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> ?S708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx = untyped_range (UntypedCap False frame pageBits idx)
 3. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> ?T708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx \<subseteq> ?S708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx
 4. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx); fst (parent_ptr, parent_idx) \<notin> ?T708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx\<rbrakk> \<Longrightarrow> frame \<le> parent_ptr \<longrightarrow> \<not> parent_ptr \<le> frame + 2 ^ pageBits - 1
 5. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pspace_aligned s \<and> valid_objs s \<and> (\<forall>x. (\<exists>idx. caps_of_state s (?slot435 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) = Some (UntypedCap (?dev437 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) \<and> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev frame pageBits f) \<and> descendants_range (UntypedCap dev frame pageBits f) (a, b) s) \<and> \<not> ?dev452 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x \<and> descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame)
 6. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits proof (prove)
goal (5 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> ?S708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx = untyped_range (UntypedCap False frame pageBits idx)
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> ?T708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx \<subseteq> ?S708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx
 3. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx); fst (parent_ptr, parent_idx) \<notin> ?T708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx\<rbrakk> \<Longrightarrow> frame \<le> parent_ptr \<longrightarrow> \<not> parent_ptr \<le> frame + 2 ^ pageBits - 1
 4. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pspace_aligned s \<and> valid_objs s \<and> (\<forall>x. (\<exists>idx. caps_of_state s (?slot435 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) = Some (UntypedCap (?dev437 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) \<and> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev frame pageBits f) \<and> descendants_range (UntypedCap dev frame pageBits f) (a, b) s) \<and> \<not> ?dev452 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x \<and> descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame)
 5. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits proof (prove)
goal (4 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> ?T708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx \<subseteq> untyped_range (UntypedCap False frame pageBits idx)
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx); fst (parent_ptr, parent_idx) \<notin> ?T708 s frame slot_ptr slot_idx parent_ptr parent_idx base idx\<rbrakk> \<Longrightarrow> frame \<le> parent_ptr \<longrightarrow> \<not> parent_ptr \<le> frame + 2 ^ pageBits - 1
 3. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pspace_aligned s \<and> valid_objs s \<and> (\<forall>x. (\<exists>idx. caps_of_state s (?slot435 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) = Some (UntypedCap (?dev437 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) \<and> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev frame pageBits f) \<and> descendants_range (UntypedCap dev frame pageBits f) (a, b) s) \<and> \<not> ?dev452 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x \<and> descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame)
 4. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits proof (prove)
goal (3 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx); fst (parent_ptr, parent_idx) \<notin> untyped_range (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> frame \<le> parent_ptr \<longrightarrow> \<not> parent_ptr \<le> frame + 2 ^ pageBits - 1
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pspace_aligned s \<and> valid_objs s \<and> (\<forall>x. (\<exists>idx. caps_of_state s (?slot435 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) = Some (UntypedCap (?dev437 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) \<and> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev frame pageBits f) \<and> descendants_range (UntypedCap dev frame pageBits f) (a, b) s) \<and> \<not> ?dev452 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x \<and> descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame)
 3. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits proof (prove)
goal (2 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> pspace_aligned s \<and> valid_objs s \<and> (\<forall>x. (\<exists>idx. caps_of_state s (?slot435 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) = Some (UntypedCap (?dev437 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) \<and> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev frame pageBits f) \<and> descendants_range (UntypedCap dev frame pageBits f) (a, b) s) \<and> \<not> ?dev452 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x \<and> descendants_range_in {frame..frame + 2 ^ pageBits - 1} (parent_ptr, parent_idx) s \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame)
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits proof (prove)
goal (2 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> (\<exists>idx. caps_of_state s (?slot435 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) = Some (UntypedCap (?dev437 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) \<and> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev frame pageBits f)) \<and> descendants_range_in {frame..frame + 2 ^ pageBits - 1} (a, b) s) \<and> \<not> ?dev452 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits proof (prove)
goal (2 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> (\<exists>idx. caps_of_state s (?slot435 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) = Some (UntypedCap (?dev437 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) base x) frame pageBits idx)) \<and> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev frame pageBits f)) \<and> descendants_range_in {frame..frame + 2 ^ pageBits - 1} (a, b) s) \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits
flex-flex pairs:
\<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t738 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) \<equiv>\<^sup>? \<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t737 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) proof (prove)
goal (2 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev frame pageBits f)) \<and> descendants_range_in {frame..frame + 2 ^ pageBits - 1} (a, b) s) \<and> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits
flex-flex pairs:
\<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t738 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) \<equiv>\<^sup>? \<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t737 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) proof (prove)
goal (2 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits
flex-flex pairs:
\<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t738 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) \<equiv>\<^sup>? \<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t737 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) proof (prove)
goal (3 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> range_cover frame pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0)
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame
 3. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits
flex-flex pairs:
\<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t738 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) \<equiv>\<^sup>? \<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t737 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) proof (prove)
goal (3 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> pageBits < 32 \<and> unat (frame && mask pageBits >> pageBits) = 0
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame
 3. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits
flex-flex pairs:
\<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t738 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) \<equiv>\<^sup>? \<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t737 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) proof (prove)
goal (3 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> pageBits < 32 \<and> unat ((frame && ~~ mask pageBits) && mask pageBits >> pageBits) = 0
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame
 3. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits
flex-flex pairs:
\<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t738 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) \<equiv>\<^sup>? \<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t737 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) proof (prove)
goal (2 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits
flex-flex pairs:
\<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t738 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) \<equiv>\<^sup>? \<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t737 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) proof (prove)
goal (2 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> (\<forall>auth\<in>cap_auth_conferred (ArchObjectCap (ASIDPoolCap frame base)). (pasSubject aag, auth, pasObjectAbs aag frame) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap frame base)) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits
flex-flex pairs:
\<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t738 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) \<equiv>\<^sup>? \<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t737 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) proof (prove)
goal (3 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx)\<rbrakk> \<Longrightarrow> frame \<in> {frame..frame + 2 ^ pageBits - 1}
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx); is_subject aag frame\<rbrakk> \<Longrightarrow> (\<forall>auth\<in>cap_auth_conferred (ArchObjectCap (ASIDPoolCap frame base)). (pasSubject aag, auth, pasObjectAbs aag frame) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap frame base)) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame
 3. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits
flex-flex pairs:
\<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t738 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) \<equiv>\<^sup>? \<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t737 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) proof (prove)
goal (2 subgoals):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base idx. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; caps_of_state s (slot_ptr, slot_idx) = Some NullCap; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None; is_aligned frame pageBits; caps_of_state s (parent_ptr, parent_idx) = Some (UntypedCap False frame pageBits idx); is_subject aag frame\<rbrakk> \<Longrightarrow> (\<forall>auth\<in>cap_auth_conferred (ArchObjectCap (ASIDPoolCap frame base)). (pasSubject aag, auth, pasObjectAbs aag frame) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap frame base)) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap frame base)) \<and> is_subject aag frame
 2. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits
flex-flex pairs:
\<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t738 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) \<equiv>\<^sup>? \<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t737 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) proof (prove)
goal (1 subgoal):
 1. \<And>s frame slot_ptr slot_idx parent_ptr parent_idx base. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; aci = MakePool frame (slot_ptr, slot_idx) (parent_ptr, parent_idx) base; cte_wp_at (\<lambda>c. c = NullCap) (slot_ptr, slot_idx) s; is_subject aag slot_ptr; cap_table_at (length slot_idx) slot_ptr s; is_aligned frame pageBits; ex_cte_cap_wp_to is_cnode_cap (slot_ptr, slot_idx) s; \<forall>asid. is_subject_asid aag asid; slot_ptr = parent_ptr \<longrightarrow> slot_idx \<noteq> parent_idx; is_subject aag parent_ptr; \<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx) (parent_ptr, parent_idx) s; descendants_of (parent_ptr, parent_idx) (cdt s) = {}; is_aligned base local.asid_low_bits; base < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of base) = None\<rbrakk> \<Longrightarrow> is_aligned frame pageBits
flex-flex pairs:
\<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t738 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) \<equiv>\<^sup>? \<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t737 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) proof (prove)
goal:
No subgoals!
flex-flex pairs:
\<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t738 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx) \<equiv>\<^sup>? \<lambda>frame slot_ptr slot_idx parent_ptr parent_idx. ?t737 frame slot_ptr slot_idx parent_ptr parent_idx (slot_ptr, slot_idx) (parent_ptr, parent_idx)