theory ArchArch_IF

lemma perform_asid_control_invocation_globals_equiv:
  notes delete_objects_invs[wp del]
  notes blah[simp del] =  atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
  shows "\<lbrace>globals_equiv s and invs and ct_active and valid_aci aci\<rbrace>
         perform_asid_control_invocation aci
         \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding perform_asid_control_invocation_def apply (rule hoare_pre) apply wpc apply (rename_tac word1 cslot_ptr1 cslot_ptr2 word2) apply (wp modify_wp cap_insert_globals_equiv''
             retype_region_ASIDPoolObj_globals_equiv[simplified]
             retype_region_invs_extras(5)[where sz=pageBits]
             retype_region_invs_extras(6)[where sz=pageBits]
             set_cap_globals_equiv
             max_index_upd_invs_simple set_cap_no_overlap
             set_cap_caps_no_overlap max_index_upd_caps_overlap_reserved
             region_in_kernel_window_preserved
             hoare_vcg_all_lift  get_cap_wp hoare_weak_lift_imp
             set_cap_idx_up_aligned_area[where dev = False,simplified]
          | simp)+ 
   (* factor out the implication -- we know what the relevant components of the
      cap referred to in the cte_wp_at are anyway from valid_aci, so just use
      those directly to simplify the reasoning later on *)
    apply (rule_tac Q="\<lambda>a b. globals_equiv s b \<and> invs b \<and>
                             word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and>
                             (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and>
                             descendants_of cslot_ptr2 (cdt b) = {} \<and>
                             pspace_no_overlap_range_cover word1 pageBits b"
                in hoare_strengthen_post) prefer 2 apply (clarsimp simp: globals_equiv_def invs_valid_global_objs) apply (drule cte_wp_at_eqD2, assumption) apply clarsimp apply (clarsimp simp: empty_descendants_range_in) apply (rule conjI, fastforce simp: cte_wp_at_def) apply (clarsimp simp: obj_bits_api_def default_arch_object_def) apply (frule untyped_cap_aligned, simp add: invs_valid_objs) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (strengthen refl caps_region_kernel_window_imp[mk_strg I E]) apply (simp add: invs_valid_objs invs_cap_refs_in_kernel_window
                     atLeastatMost_subset_iff word_and_le2
               cong: conj_cong) apply (rule conjI, rule descendants_range_caps_no_overlapI) apply assumption apply (simp add: cte_wp_at_caps_of_state) apply (simp add: empty_descendants_range_in) apply (clarsimp simp: range_cover_def) apply (subst is_aligned_neg_mask_eq[THEN sym], assumption) apply (simp add: word_bw_assocs pageBits_def mask_zero) apply (wp add: delete_objects_invs_ex delete_objects_pspace_no_overlap[where dev=False]
                  delete_objects_globals_equiv hoare_vcg_ex_lift
             del: Untyped_AI.delete_objects_pspace_no_overlap
          | simp add: page_bits_def)+ apply (clarsimp simp: conj_comms
                        invs_psp_aligned invs_valid_objs valid_aci_def) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (frule_tac cap="UntypedCap False a b c" for a b c in caps_of_state_valid, assumption) apply (clarsimp simp: valid_cap_def cap_aligned_def untyped_min_bits_def) apply (frule_tac slot="(aa,ba)"
                in untyped_caps_do_not_overlap_global_refs[rotated, OF invs_valid_global_refs]) apply (clarsimp simp: cte_wp_at_caps_of_state) apply ((rule conjI |rule refl | simp)+)[1] apply (rule conjI) apply (clarsimp simp: global_refs_def ptr_range_memI) apply (rule conjI) apply (clarsimp simp: global_refs_def ptr_range_memI) apply (rule conjI, fastforce simp: global_refs_def) apply (rule conjI, fastforce simp: global_refs_def) apply (rule conjI) apply (drule untyped_slots_not_in_untyped_range) apply (blast intro!: empty_descendants_range_in) apply (simp add: cte_wp_at_caps_of_state) apply simp apply (rule refl) apply (rule subset_refl) apply (simp) apply (rule conjI) apply fastforce apply (auto intro: empty_descendants_range_in simp: descendants_range_def2 cap_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and invs and ct_active and valid_aci aci\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and invs and ct_active and valid_aci 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>_. globals_equiv s\<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>_. globals_equiv s\<rbrace>
 2. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> ?Q sa proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?R12 x1 x2 x3 x4\<rbrace> do delete_objects x1 page_bits;
pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2;
assert (x4 && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?R12 x xa xb xc sa proof (prove)
goal (2 subgoals):
 1. \<And>word1 cslot_ptr1 cslot_ptr2 word2. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?R12 word1 cslot_ptr1 cslot_ptr2 word2\<rbrace> do delete_objects word1 page_bits;
pcap <- get_cap cslot_ptr2;
set_cap (max_free_index_update pcap) cslot_ptr2;
retype_region word1 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap word1 word2) cslot_ptr2 cslot_ptr1;
assert (word2 && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of word2 \<mapsto> word1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?R12 x xa xb xc sa proof (prove)
goal (2 subgoals):
 1. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>rv sa. cte_wp_at ((=) cap) cslot_ptr2 sa \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> globals_equiv s sa \<and> valid_global_objs sa \<and> valid_arch_state sa \<and> word1 \<noteq> arm_global_pd (arch_state s) \<and> word1 \<noteq> idle_thread sa \<and> descendants_range_in (untyped_range cap) cslot_ptr2 sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> invs sa \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area word1 pageBits) sa \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) cslot_ptr2 sa \<and> caps_no_overlap word1 pageBits sa \<and> invs sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} cslot_ptr2 sa \<and> is_untyped_cap cap \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> (\<exists>idx. cap = UntypedCap False word1 pageBits idx) \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) cslot_ptr2 sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> invs sa \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area word1 pageBits) sa \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) cslot_ptr2 sa \<and> caps_no_overlap word1 pageBits sa \<and> invs sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} cslot_ptr2 sa \<and> is_untyped_cap cap \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> (\<exists>idx. cap = UntypedCap False word1 pageBits idx) \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0)\<rbrace>
 2. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (2 subgoals):
 1. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>rv sa. cte_wp_at ((=) cap) cslot_ptr2 sa \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> globals_equiv s sa \<and> valid_global_objs sa \<and> valid_arch_state sa \<and> word1 \<noteq> arm_global_pd (arch_state s) \<and> word1 \<noteq> idle_thread sa \<and> descendants_range_in (untyped_range cap) cslot_ptr2 sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> invs sa \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area word1 pageBits) sa \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) cslot_ptr2 sa \<and> caps_no_overlap word1 pageBits sa \<and> invs sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} cslot_ptr2 sa \<and> is_untyped_cap cap \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> (\<exists>idx. cap = UntypedCap False word1 pageBits idx) \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) cslot_ptr2 sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> invs sa \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area word1 pageBits) sa \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) cslot_ptr2 sa \<and> caps_no_overlap word1 pageBits sa \<and> invs sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} cslot_ptr2 sa \<and> is_untyped_cap cap \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> (\<exists>idx. cap = UntypedCap False word1 pageBits idx) \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0)\<rbrace>
 2. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap rv sa. \<lbrakk>aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2; globals_equiv s sa \<and> invs sa \<and> word1 \<noteq> arm_global_pd (arch_state sa) \<and> word1 \<noteq> idle_thread sa \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 sa) \<and> descendants_of cslot_ptr2 (cdt sa) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) sa\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) cslot_ptr2 sa \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> globals_equiv s sa \<and> valid_global_objs sa \<and> valid_arch_state sa \<and> word1 \<noteq> arm_global_pd (arch_state s) \<and> word1 \<noteq> idle_thread sa \<and> descendants_range_in (untyped_range cap) cslot_ptr2 sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> invs sa \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area word1 pageBits) sa \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) cslot_ptr2 sa \<and> caps_no_overlap word1 pageBits sa \<and> invs sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} cslot_ptr2 sa \<and> is_untyped_cap cap \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> (\<exists>idx. cap = UntypedCap False word1 pageBits idx) \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) cslot_ptr2 sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> invs sa \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area word1 pageBits) sa \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) cslot_ptr2 sa \<and> caps_no_overlap word1 pageBits sa \<and> invs sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} cslot_ptr2 sa \<and> is_untyped_cap cap \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> (\<exists>idx. cap = UntypedCap False word1 pageBits idx) \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0)
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap rv sa. \<lbrakk>aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2; globals_equiv s sa \<and> invs sa \<and> word1 \<noteq> arm_global_pd (arch_state sa) \<and> word1 \<noteq> idle_thread sa \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 sa) \<and> descendants_of cslot_ptr2 (cdt sa) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) sa\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) cslot_ptr2 sa \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> globals_equiv s sa \<and> valid_global_objs sa \<and> valid_arch_state sa \<and> word1 \<noteq> arm_global_pd (arch_state s) \<and> word1 \<noteq> idle_thread sa \<and> descendants_range_in (untyped_range cap) cslot_ptr2 sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> invs sa \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area word1 pageBits) sa \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) cslot_ptr2 sa \<and> caps_no_overlap word1 pageBits sa \<and> invs sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} cslot_ptr2 sa \<and> is_untyped_cap cap \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> (\<exists>idx. cap = UntypedCap False word1 pageBits idx) \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) cslot_ptr2 sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> invs sa \<and> is_untyped_cap cap \<and> pspace_no_overlap (up_aligned_area word1 pageBits) sa \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) cslot_ptr2 sa \<and> caps_no_overlap word1 pageBits sa \<and> invs sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} cslot_ptr2 sa \<and> is_untyped_cap cap \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> (\<exists>idx. cap = UntypedCap False word1 pageBits idx) \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0)
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 cap sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap (up_aligned_area word1 pageBits) sa; cte_wp_at ((=) cap) (aa, ba) sa; word2 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> valid_arch_state sa \<and> descendants_range_in (untyped_range cap) (aa, ba) sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (aa, ba) sa \<and> caps_no_overlap word1 pageBits sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (aa, ba) sa \<and> is_untyped_cap cap \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> (\<exists>idx. cap = UntypedCap False word1 pageBits idx) \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (aa, ba) sa \<and> caps_no_overlap word1 pageBits sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (aa, ba) sa \<and> is_untyped_cap cap \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> (\<exists>idx. cap = UntypedCap False word1 pageBits idx) \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0)
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 cap sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap (up_aligned_area word1 pageBits) sa; cte_wp_at ((=) cap) (aa, ba) sa; word2 && mask local.asid_low_bits = 0; cap = UntypedCap False word1 pageBits idx\<rbrakk> \<Longrightarrow> valid_arch_state sa \<and> descendants_range_in (untyped_range cap) (aa, ba) sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (aa, ba) sa \<and> caps_no_overlap word1 pageBits sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (aa, ba) sa \<and> is_untyped_cap cap \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> (\<exists>idx. cap = UntypedCap False word1 pageBits idx) \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) sa \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) sa \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) (aa, ba) sa \<and> caps_no_overlap word1 pageBits sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> untyped_range cap \<and> descendants_range_in {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (aa, ba) sa \<and> is_untyped_cap cap \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> (\<exists>idx. cap = UntypedCap False word1 pageBits idx) \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0)
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap (up_aligned_area word1 pageBits) sa; cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) (aa, ba) sa; word2 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> valid_arch_state sa \<and> descendants_range_in {word1..word1 + 2 ^ pageBits - 1} (aa, ba) sa \<and> cte_wp_at (\<lambda>c. untyped_range c = {word1..word1 + 2 ^ pageBits - 1}) (aa, ba) sa \<and> caps_no_overlap word1 pageBits sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> {word1..word1 + 2 ^ pageBits - 1} \<and> descendants_range_in {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (aa, ba) sa \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in {word1..word1 + 2 ^ pageBits - 1} (aa, ba) sa \<and> cte_wp_at (\<lambda>c. untyped_range c = {word1..word1 + 2 ^ pageBits - 1}) (aa, ba) sa \<and> caps_no_overlap word1 pageBits sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> {word1..word1 + 2 ^ pageBits - 1} \<and> descendants_range_in {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} (aa, ba) sa \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0)
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap (up_aligned_area word1 pageBits) sa; cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) (aa, ba) sa; word2 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> valid_arch_state sa \<and> cte_wp_at (\<lambda>c. untyped_range c = {word1..word1 + 2 ^ pageBits - 1}) (aa, ba) sa \<and> caps_no_overlap word1 pageBits sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> {word1..word1 + 2 ^ pageBits - 1} \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> cte_wp_at (\<lambda>c. untyped_range c = {word1..word1 + 2 ^ pageBits - 1}) (aa, ba) sa \<and> caps_no_overlap word1 pageBits sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> {word1..word1 + 2 ^ pageBits - 1} \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0)
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap (up_aligned_area word1 pageBits) sa; cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) (aa, ba) sa; word2 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. untyped_range c = {word1..word1 + 2 ^ pageBits - 1}) (aa, ba) sa \<and> caps_no_overlap word1 pageBits sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> {word1..word1 + 2 ^ pageBits - 1} \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> cte_wp_at (\<lambda>c. untyped_range c = {word1..word1 + 2 ^ pageBits - 1}) (aa, ba) sa \<and> caps_no_overlap word1 pageBits sa \<and> {word1..word1 + 2 ^ obj_bits_api (ArchObject ASIDPoolObj) 0 - 1} \<subseteq> {word1..word1 + 2 ^ pageBits - 1} \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> valid_objs sa \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0)
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap (up_aligned_area word1 pageBits) sa; cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) (aa, ba) sa; word2 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. untyped_range c = {word1..word1 + 2 ^ pageBits - 1}) (aa, ba) sa \<and> caps_no_overlap word1 pageBits sa \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> valid_objs sa \<and> range_cover word1 pageBits pageBits (Suc 0) \<and> cte_wp_at (\<lambda>c. untyped_range c = {word1..word1 + 2 ^ pageBits - 1}) (aa, ba) sa \<and> caps_no_overlap word1 pageBits sa \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> valid_objs sa \<and> range_cover word1 pageBits pageBits (Suc 0)
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap (up_aligned_area word1 pageBits) sa; cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) (aa, ba) sa; word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. untyped_range c = {word1..word1 + 2 ^ pageBits - 1}) (aa, ba) sa \<and> caps_no_overlap word1 pageBits sa \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> valid_objs sa \<and> range_cover word1 pageBits pageBits (Suc 0) \<and> cte_wp_at (\<lambda>c. untyped_range c = {word1..word1 + 2 ^ pageBits - 1}) (aa, ba) sa \<and> caps_no_overlap word1 pageBits sa \<and> region_in_kernel_window {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} sa \<and> valid_objs sa \<and> range_cover word1 pageBits pageBits (Suc 0)
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> caps_no_overlap word1 pageBits sa \<and> region_in_kernel_window {word1..word1 + 2 ^ pageBits - 1} sa \<and> valid_objs sa \<and> range_cover word1 pageBits pageBits (Suc 0) \<and> caps_no_overlap word1 pageBits sa \<and> region_in_kernel_window {word1..word1 + 2 ^ pageBits - 1} sa \<and> valid_objs sa \<and> range_cover word1 pageBits pageBits (Suc 0)
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> caps_no_overlap word1 pageBits sa \<and> (cap_refs_in_kernel_window sa \<and> {word1..word1 + 2 ^ pageBits - 1} \<subseteq> cap_range (UntypedCap False word1 pageBits idx)) \<and> valid_objs sa \<and> range_cover word1 pageBits pageBits (Suc 0) \<and> caps_no_overlap word1 pageBits sa \<and> (cap_refs_in_kernel_window sa \<and> {word1..word1 + 2 ^ pageBits - 1} \<subseteq> cap_range (UntypedCap False word1 pageBits idx)) \<and> valid_objs sa \<and> range_cover word1 pageBits pageBits (Suc 0)
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> caps_no_overlap word1 pageBits sa \<and> range_cover word1 pageBits pageBits (Suc 0)
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (6 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> invs sa
 2. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (UntypedCap (?dev191 word1 a b aa ba word2 sa idx) (word1 && ~~ mask pageBits) pageBits (?idx191 word1 a b aa ba word2 sa idx))) (?cref191 word1 a b aa ba word2 sa idx) sa
 3. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> descendants_range_in {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} (?cref191 word1 a b aa ba word2 sa idx) sa
 4. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> range_cover word1 pageBits pageBits (Suc 0)
 5. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 6. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (5 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (UntypedCap (?dev191 word1 a b aa ba word2 sa idx) (word1 && ~~ mask pageBits) pageBits (?idx191 word1 a b aa ba word2 sa idx))) (?cref191 word1 a b aa ba word2 sa idx) sa
 2. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> descendants_range_in {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} (?cref191 word1 a b aa ba word2 sa idx) sa
 3. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> range_cover word1 pageBits pageBits (Suc 0)
 4. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 5. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (4 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> descendants_range_in {word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} (aa, ba) sa
 2. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> range_cover word1 pageBits pageBits (Suc 0)
 3. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 4. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> range_cover word1 pageBits pageBits (Suc 0)
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> pageBits < 32 \<and> unat (word1 && mask pageBits >> pageBits) = 0
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_equiv s sa; cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa)); invs sa; word1 \<noteq> arm_global_pd (arch_state sa); word1 \<noteq> idle_thread sa; descendants_of (aa, ba) (cdt sa) = {}; pspace_no_overlap {word1..word1 + (2 ^ pageBits - 1)} sa; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word2 && mask local.asid_low_bits = 0; is_aligned word1 pageBits\<rbrakk> \<Longrightarrow> pageBits < 32 \<and> unat ((word1 && ~~ mask pageBits) && mask pageBits >> pageBits) = 0
 2. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 3. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (2 subgoals):
 1. \<And>word1 cslot_ptr1 cslot_ptr2 word2 cap. aci = MakePool word1 cslot_ptr1 cslot_ptr2 word2 \<Longrightarrow> \<lbrace>?P125 word1 cslot_ptr1 cslot_ptr2 word2 cap\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>a b. globals_equiv s b \<and> invs b \<and> word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and> descendants_of cslot_ptr2 (cdt b) = {} \<and> pspace_no_overlap (up_aligned_area word1 pageBits) b\<rbrace>
 2. \<And>sa. (globals_equiv s and invs and ct_active and valid_aci aci) sa \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> (\<forall>xd. ?P125 x xa xb xc xd sa) proof (prove)
goal (1 subgoal):
 1. \<And>sa. globals_equiv s sa \<and> invs sa \<and> ct_active sa \<and> valid_aci aci sa \<Longrightarrow> \<forall>x a b aa ba xa. aci = MakePool x (a, b) (aa, ba) xa \<longrightarrow> is_aligned x pageBits \<and> 2 \<le> pageBits \<and> arm_global_pd (arch_state sa) \<notin> ptr_range x pageBits \<and> idle_thread sa \<notin> ptr_range x pageBits \<and> (\<exists>a b dev f. cte_wp_at ((=) (UntypedCap dev x pageBits f)) (a, b) sa \<and> descendants_range (UntypedCap dev x pageBits f) (a, b) sa) \<and> x \<noteq> arm_global_pd (arch_state sa) \<and> x \<noteq> idle_thread sa \<and> (\<exists>xa. cte_wp_at ((=) (UntypedCap False x pageBits xa)) (aa, ba) sa) \<and> aa \<notin> {x..x + 2 ^ pageBits - 1} \<and> descendants_of (aa, ba) (cdt sa) = {} \<and> pspace_aligned sa \<and> valid_objs sa \<and> (\<forall>xb. \<exists>idx. cte_wp_at ((=) (UntypedCap False x pageBits idx)) (?slot217 x (a, b) (aa, ba) xa xb) sa) proof (prove)
goal (1 subgoal):
 1. \<And>sa x a b aa ba xa. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) sa\<rbrakk> \<Longrightarrow> is_aligned x pageBits \<and> x \<noteq> idle_thread sa \<and> 2 \<le> pageBits \<and> x \<noteq> arm_global_pd (arch_state sa) \<and> idle_thread sa \<notin> ptr_range x pageBits \<and> arm_global_pd (arch_state sa) \<notin> ptr_range x pageBits \<and> (\<exists>xa. cte_wp_at ((=) (UntypedCap False x pageBits xa)) (aa, ba) sa) \<and> aa \<notin> {x..x + 2 ^ pageBits - 1} \<and> (\<forall>xb. \<exists>idx. cte_wp_at ((=) (UntypedCap False x pageBits idx)) (?slot217 x (a, b) (aa, ba) xa xb) sa) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> cte_wp_at ((=) (UntypedCap dev x pageBits f)) (a, b) sa) proof (prove)
goal (1 subgoal):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx)\<rbrakk> \<Longrightarrow> is_aligned x pageBits \<and> x \<noteq> idle_thread sa \<and> 2 \<le> pageBits \<and> x \<noteq> arm_global_pd (arch_state sa) \<and> idle_thread sa \<notin> ptr_range x pageBits \<and> arm_global_pd (arch_state sa) \<notin> ptr_range x pageBits \<and> aa \<notin> {x..x + 2 ^ pageBits - 1} \<and> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (1 subgoal):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); sa \<turnstile> UntypedCap False x pageBits idx\<rbrakk> \<Longrightarrow> is_aligned x pageBits \<and> x \<noteq> idle_thread sa \<and> 2 \<le> pageBits \<and> x \<noteq> arm_global_pd (arch_state sa) \<and> idle_thread sa \<notin> ptr_range x pageBits \<and> arm_global_pd (arch_state sa) \<notin> ptr_range x pageBits \<and> aa \<notin> {x..x + 2 ^ pageBits - 1} \<and> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (1 subgoal):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread sa \<and> x \<noteq> arm_global_pd (arch_state sa) \<and> idle_thread sa \<notin> ptr_range x pageBits \<and> arm_global_pd (arch_state sa) \<notin> ptr_range x pageBits \<and> aa \<notin> {x..x + 2 ^ pageBits - 1} \<and> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (2 subgoals):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (UntypedCap (?dev256 sa x a b aa ba xa idx) (?word256 sa x a b aa ba xa idx) (?sz256 sa x a b aa ba xa idx) (?idx256 sa x a b aa ba xa idx))) (aa, ba) sa
 2. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range (?word256 sa x a b aa ba xa idx) (?sz256 sa x a b aa ba xa idx) \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread sa \<and> x \<noteq> arm_global_pd (arch_state sa) \<and> idle_thread sa \<notin> ptr_range x pageBits \<and> arm_global_pd (arch_state sa) \<notin> ptr_range x pageBits \<and> aa \<notin> {x..x + 2 ^ pageBits - 1} \<and> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (2 subgoals):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> ?dev256 sa x a b aa ba xa idx \<and> ?word256 sa x a b aa ba xa idx = x \<and> ?sz256 sa x a b aa ba xa idx = pageBits \<and> ?idx256 sa x a b aa ba xa idx = idx
 2. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range (?word256 sa x a b aa ba xa idx) (?sz256 sa x a b aa ba xa idx) \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread sa \<and> x \<noteq> arm_global_pd (arch_state sa) \<and> idle_thread sa \<notin> ptr_range x pageBits \<and> arm_global_pd (arch_state sa) \<notin> ptr_range x pageBits \<and> aa \<notin> {x..x + 2 ^ pageBits - 1} \<and> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (1 subgoal):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread sa \<and> x \<noteq> arm_global_pd (arch_state sa) \<and> idle_thread sa \<notin> ptr_range x pageBits \<and> arm_global_pd (arch_state sa) \<notin> ptr_range x pageBits \<and> aa \<notin> {x..x + 2 ^ pageBits - 1} \<and> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (2 subgoals):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread sa
 2. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> x \<noteq> arm_global_pd (arch_state sa) \<and> idle_thread sa \<notin> ptr_range x pageBits \<and> arm_global_pd (arch_state sa) \<notin> ptr_range x pageBits \<and> aa \<notin> {x..x + 2 ^ pageBits - 1} \<and> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (1 subgoal):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> x \<noteq> arm_global_pd (arch_state sa) \<and> idle_thread sa \<notin> ptr_range x pageBits \<and> arm_global_pd (arch_state sa) \<notin> ptr_range x pageBits \<and> aa \<notin> {x..x + 2 ^ pageBits - 1} \<and> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (2 subgoals):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> x \<noteq> arm_global_pd (arch_state sa)
 2. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> idle_thread sa \<notin> ptr_range x pageBits \<and> arm_global_pd (arch_state sa) \<notin> ptr_range x pageBits \<and> aa \<notin> {x..x + 2 ^ pageBits - 1} \<and> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (1 subgoal):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> idle_thread sa \<notin> ptr_range x pageBits \<and> arm_global_pd (arch_state sa) \<notin> ptr_range x pageBits \<and> aa \<notin> {x..x + 2 ^ pageBits - 1} \<and> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (1 subgoal):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state sa) \<notin> ptr_range x pageBits \<and> aa \<notin> {x..x + 2 ^ pageBits - 1} \<and> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (1 subgoal):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> aa \<notin> {x..x + 2 ^ pageBits - 1} \<and> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (2 subgoals):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> aa \<notin> {x..x + 2 ^ pageBits - 1}
 2. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (7 subgoals):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> descendants_range_in (?S310 sa x a b aa ba xa idx) (?slot310 sa x a b aa ba xa idx) sa
 2. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap310 sa x a b aa ba xa idx)) (?slot310 sa x a b aa ba xa idx) sa
 3. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> is_untyped_cap (?cap310 sa x a b aa ba xa idx)
 4. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> ?S310 sa x a b aa ba xa idx = untyped_range (?cap310 sa x a b aa ba xa idx)
 5. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> ?T310 sa x a b aa ba xa idx \<subseteq> ?S310 sa x a b aa ba xa idx
 6. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}; fst (?slot310 sa x a b aa ba xa idx) \<notin> ?T310 sa x a b aa ba xa idx\<rbrakk> \<Longrightarrow> aa \<notin> {x..x + 2 ^ pageBits - 1}
 7. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (6 subgoals):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap310 sa x a b aa ba xa idx)) (aa, ba) sa
 2. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> is_untyped_cap (?cap310 sa x a b aa ba xa idx)
 3. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> ?S310 sa x a b aa ba xa idx = untyped_range (?cap310 sa x a b aa ba xa idx)
 4. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> ?T310 sa x a b aa ba xa idx \<subseteq> ?S310 sa x a b aa ba xa idx
 5. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}; fst (aa, ba) \<notin> ?T310 sa x a b aa ba xa idx\<rbrakk> \<Longrightarrow> aa \<notin> {x..x + 2 ^ pageBits - 1}
 6. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (5 subgoals):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> is_untyped_cap (UntypedCap False x pageBits idx)
 2. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> ?S310 sa x a b aa ba xa idx = untyped_range (UntypedCap False x pageBits idx)
 3. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> ?T310 sa x a b aa ba xa idx \<subseteq> ?S310 sa x a b aa ba xa idx
 4. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}; fst (aa, ba) \<notin> ?T310 sa x a b aa ba xa idx\<rbrakk> \<Longrightarrow> aa \<notin> {x..x + 2 ^ pageBits - 1}
 5. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (4 subgoals):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> ?S310 sa x a b aa ba xa idx = untyped_range (UntypedCap False x pageBits idx)
 2. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> ?T310 sa x a b aa ba xa idx \<subseteq> ?S310 sa x a b aa ba xa idx
 3. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}; fst (aa, ba) \<notin> ?T310 sa x a b aa ba xa idx\<rbrakk> \<Longrightarrow> aa \<notin> {x..x + 2 ^ pageBits - 1}
 4. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (3 subgoals):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> ?T310 sa x a b aa ba xa idx \<subseteq> untyped_range (UntypedCap False x pageBits idx)
 2. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}; fst (aa, ba) \<notin> ?T310 sa x a b aa ba xa idx\<rbrakk> \<Longrightarrow> aa \<notin> {x..x + 2 ^ pageBits - 1}
 3. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (2 subgoals):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}; fst (aa, ba) \<notin> untyped_range (UntypedCap False x pageBits idx)\<rbrakk> \<Longrightarrow> aa \<notin> {x..x + 2 ^ pageBits - 1}
 2. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (1 subgoal):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> (\<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)) \<and> (\<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f)) proof (prove)
goal (2 subgoals):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> \<forall>xb. \<exists>idx. caps_of_state sa (?slot217 x (a, b) (aa, ba) xa xb) = Some (UntypedCap False x pageBits idx)
 2. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> \<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f) proof (prove)
goal (1 subgoal):
 1. \<And>sa x a b aa ba xa idx. \<lbrakk>invs sa; globals_equiv s sa; ct_active sa; aci = MakePool x (a, b) (aa, ba) xa; is_aligned xa local.asid_low_bits; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; asid_table sa (asid_high_bits_of xa) = None; xa < 2 ^ local.asid_bits; descendants_of (aa, ba) (cdt sa) = {}; b = ba \<longrightarrow> a \<noteq> aa; caps_of_state sa (a, b) = Some NullCap; caps_of_state sa (aa, ba) = Some (UntypedCap False x pageBits idx); is_aligned x pageBits; valid_untyped (UntypedCap False x pageBits idx) sa; 4 \<le> pageBits; idx \<le> 2 ^ pageBits; x \<noteq> 0; ptr_range x pageBits \<inter> global_refs sa = {}\<rbrakk> \<Longrightarrow> \<exists>a b dev f. descendants_range (UntypedCap dev x pageBits f) (a, b) sa \<and> caps_of_state sa (a, b) = Some (UntypedCap dev x pageBits f) proof (prove)
goal:
No subgoals!