theory ArchArch_AI

lemma perform_asid_control_invocation_pred_tcb_at:
  "\<lbrace>\<lambda>s. pred_tcb_at proj Q t s \<and> st_tcb_at ((Not \<circ> inactive) and (Not \<circ> idle)) t s
        \<and> ct_active s \<and> invs s \<and> valid_aci aci s\<rbrace>
   perform_asid_control_invocation aci
   \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace>" including no_pre supply
    is_aligned_neg_mask_eq[simp del]
    is_aligned_neg_mask_weaken[simp del] apply (clarsimp simp: perform_asid_control_invocation_def split: asid_control_invocation.splits) apply (rename_tac word1 a b aa ba word2) apply (wp hoare_vcg_const_imp_lift retype_region_st_tcb_at set_cap_no_overlap|simp)+ apply (strengthen invs_valid_objs invs_psp_aligned) apply (clarsimp simp:conj_comms) apply (wp max_index_upd_invs_simple get_cap_wp)+ apply (rule hoare_name_pre_state) apply (subgoal_tac "is_aligned word1 page_bits") prefer 2 apply (clarsimp simp: valid_aci_def cte_wp_at_caps_of_state) apply (drule(1) caps_of_state_valid[rotated])+ apply (simp add:valid_cap_simps cap_aligned_def page_bits_def) apply (subst delete_objects_rewrite) apply (simp add:page_bits_def word_bits_def pageBits_def word_size_bits_def)+ apply (simp add:is_aligned_neg_mask_eq) apply (rule hoare_pre, wp) apply (clarsimp simp: valid_aci_def) apply (frule intvl_range_conv) apply (simp add:word_bits_def page_bits_def pageBits_def) apply (clarsimp simp:detype_clear_um_independent page_bits_def is_aligned_neg_mask_eq) apply (rule conjI) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (rule pspace_no_overlap_detype) apply (rule caps_of_state_valid_cap) apply (simp add:page_bits_def)+ apply (simp add:invs_valid_objs invs_psp_aligned)+ apply (rule conjI) apply (frule st_tcb_ex_cap) apply clarsimp apply (clarsimp split: Structures_A.thread_state.splits) apply (clarsimp simp: ex_nonz_cap_to_def) apply (frule invs_untyped_children) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (erule_tac ptr="(aa,ba)" in untyped_children_in_mdbE[where P="\<lambda>c. t \<in> zobj_refs c" for t]) apply (simp add: cte_wp_at_caps_of_state)+ apply fastforce apply (clarsimp simp: zobj_refs_to_obj_refs) apply (fastforce simp:page_bits_def) apply simp apply (clarsimp simp:obj_bits_api_def arch_kobj_size_def cte_wp_at_caps_of_state
    default_arch_object_def empty_descendants_range_in) apply (frule_tac cap = "(cap.UntypedCap False word1 pageBits idx)"
    in detype_invariants[rotated 3],clarsimp+) apply (simp add:cte_wp_at_caps_of_state
      empty_descendants_range_in descendants_range_def2)+ apply (thin_tac "x = Some cap.NullCap" for x)+ apply (drule(1) caps_of_state_valid_cap[OF _ invs_valid_objs]) apply (intro conjI) apply (clarsimp simp:valid_cap_def cap_aligned_def range_cover_full
     invs_psp_aligned invs_valid_objs page_bits_def) apply (erule pspace_no_overlap_detype) apply (auto simp:page_bits_def detype_clear_um_independent) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci aci s\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci aci s\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci aci s\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4. aci = MakePool x1 (a, b) (aa, ba) x4 \<Longrightarrow> \<lbrace>\<lambda>s. pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool x1 (a, b) (aa, ba) x4) s\<rbrace> do y <- delete_objects x1 page_bits;
pcap <- get_cap (aa, ba);
y <- set_cap (max_free_index_update pcap) (aa, ba);
y <- retype_region x1 (Suc 0) 0 (ArchObject ASIDPoolObj) False;
y <- cap_insert (ArchObjectCap (ASIDPoolCap x1 x4)) (aa, ba) (a, b);
y <- assert (x4 && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of x4 \<mapsto> x1)\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2. aci = MakePool word1 (a, b) (aa, ba) word2 \<Longrightarrow> \<lbrace>\<lambda>s. pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s\<rbrace> do y <- delete_objects word1 page_bits;
pcap <- get_cap (aa, ba);
y <- set_cap (max_free_index_update pcap) (aa, ba);
y <- retype_region word1 (Suc 0) 0 (ArchObject ASIDPoolObj) False;
y <- cap_insert (ArchObjectCap (ASIDPoolCap word1 word2)) (aa, ba) (a, b);
y <- assert (word2 && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of word2 \<mapsto> word1)\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 pcap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; word2 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'38 word1 a b aa ba word2 () pcap\<rbrace> set_cap (max_free_index_update pcap) (aa, ba) \<lbrace>\<lambda>rv s. valid_objs s \<and> pspace_aligned s\<rbrace>
 2. \<And>word1 a b aa ba word2 y. aci = MakePool word1 (a, b) (aa, ba) word2 \<Longrightarrow> \<lbrace>?B11 word1 a b aa ba word2 y\<rbrace> get_cap (aa, ba) \<lbrace>\<lambda>pcap s. word2 && mask local.asid_low_bits = 0 \<longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz35 word1 a b aa ba word2 y pcap)) s \<and> pred_tcb_at proj Q t s \<and> range_cover word1 (?sz35 word1 a b aa ba word2 y pcap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> ?P'38 word1 a b aa ba word2 y pcap s\<rbrace>
 3. \<And>word1 a b aa ba word2. aci = MakePool word1 (a, b) (aa, ba) word2 \<Longrightarrow> \<lbrace>\<lambda>s. pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s\<rbrace> delete_objects word1 page_bits \<lbrace>?B11 word1 a b aa ba word2\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 pcap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; word2 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'38 word1 a b aa ba word2 () pcap\<rbrace> set_cap (max_free_index_update pcap) (aa, ba) \<lbrace>\<lambda>r s. invs s \<and> invs s\<rbrace>
 2. \<And>word1 a b aa ba word2 y. aci = MakePool word1 (a, b) (aa, ba) word2 \<Longrightarrow> \<lbrace>?B11 word1 a b aa ba word2 y\<rbrace> get_cap (aa, ba) \<lbrace>\<lambda>pcap s. word2 && mask local.asid_low_bits = 0 \<longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz35 word1 a b aa ba word2 y pcap)) s \<and> pred_tcb_at proj Q t s \<and> range_cover word1 (?sz35 word1 a b aa ba word2 y pcap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> ?P'38 word1 a b aa ba word2 y pcap s\<rbrace>
 3. \<And>word1 a b aa ba word2. aci = MakePool word1 (a, b) (aa, ba) word2 \<Longrightarrow> \<lbrace>\<lambda>s. pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s\<rbrace> delete_objects word1 page_bits \<lbrace>?B11 word1 a b aa ba word2\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 pcap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; word2 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'38 word1 a b aa ba word2 () pcap\<rbrace> set_cap (max_free_index_update pcap) (aa, ba) \<lbrace>\<lambda>r. invs\<rbrace>
 2. \<And>word1 a b aa ba word2 y. aci = MakePool word1 (a, b) (aa, ba) word2 \<Longrightarrow> \<lbrace>?B11 word1 a b aa ba word2 y\<rbrace> get_cap (aa, ba) \<lbrace>\<lambda>pcap s. word2 && mask local.asid_low_bits = 0 \<longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz35 word1 a b aa ba word2 y pcap)) s \<and> pred_tcb_at proj Q t s \<and> range_cover word1 (?sz35 word1 a b aa ba word2 y pcap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> ?P'38 word1 a b aa ba word2 y pcap s\<rbrace>
 3. \<And>word1 a b aa ba word2. aci = MakePool word1 (a, b) (aa, ba) word2 \<Longrightarrow> \<lbrace>\<lambda>s. pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s\<rbrace> delete_objects word1 page_bits \<lbrace>?B11 word1 a b aa ba word2\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2. aci = MakePool word1 (a, b) (aa, ba) word2 \<Longrightarrow> \<lbrace>\<lambda>s. pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>y s. \<forall>cap. cte_wp_at ((=) cap) (aa, ba) s \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz35 word1 a b aa ba word2 y cap)) s \<and> pred_tcb_at proj Q t s \<and> range_cover word1 (?sz35 word1 a b aa ba word2 y cap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> cte_wp_at ((=) cap) (aa, ba) s \<and> is_untyped_cap cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>y s. \<forall>cap. cte_wp_at ((=) cap) (aa, ba) s \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz35 word1 a b aa ba word2 y cap)) s \<and> pred_tcb_at proj Q t s \<and> range_cover word1 (?sz35 word1 a b aa ba word2 y cap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> cte_wp_at ((=) cap) (aa, ba) s \<and> is_untyped_cap cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s; is_aligned word1 page_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>y s. \<forall>cap. cte_wp_at ((=) cap) (aa, ba) s \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz35 word1 a b aa ba word2 y cap)) s \<and> pred_tcb_at proj Q t s \<and> range_cover word1 (?sz35 word1 a b aa ba word2 y cap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> cte_wp_at ((=) cap) (aa, ba) s \<and> is_untyped_cap cap\<rbrace>
 2. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s\<rbrakk> \<Longrightarrow> is_aligned word1 page_bits proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s\<rbrakk> \<Longrightarrow> is_aligned word1 page_bits
 2. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s; is_aligned word1 page_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>y s. \<forall>cap. cte_wp_at ((=) cap) (aa, ba) s \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz35 word1 a b aa ba word2 y cap)) s \<and> pred_tcb_at proj Q t s \<and> range_cover word1 (?sz35 word1 a b aa ba word2 y cap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> cte_wp_at ((=) cap) (aa, ba) s \<and> is_untyped_cap cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 s idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s; ct_active s; invs s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; caps_of_state s (aa, ba) = Some (UntypedCap False word1 pageBits idx); is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of word2) = None\<rbrakk> \<Longrightarrow> is_aligned word1 page_bits
 2. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s; is_aligned word1 page_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>y s. \<forall>cap. cte_wp_at ((=) cap) (aa, ba) s \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz35 word1 a b aa ba word2 y cap)) s \<and> pred_tcb_at proj Q t s \<and> range_cover word1 (?sz35 word1 a b aa ba word2 y cap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> cte_wp_at ((=) cap) (aa, ba) s \<and> is_untyped_cap cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 s idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s; ct_active s; invs s; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of word2) = None; s \<turnstile> NullCap; s \<turnstile> UntypedCap False word1 pageBits idx\<rbrakk> \<Longrightarrow> is_aligned word1 page_bits
 2. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s; is_aligned word1 page_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>y s. \<forall>cap. cte_wp_at ((=) cap) (aa, ba) s \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz35 word1 a b aa ba word2 y cap)) s \<and> pred_tcb_at proj Q t s \<and> range_cover word1 (?sz35 word1 a b aa ba word2 y cap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> cte_wp_at ((=) cap) (aa, ba) s \<and> is_untyped_cap cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s; is_aligned word1 page_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> delete_objects word1 page_bits \<lbrace>\<lambda>y s. \<forall>cap. cte_wp_at ((=) cap) (aa, ba) s \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz35 word1 a b aa ba word2 y cap)) s \<and> pred_tcb_at proj Q t s \<and> range_cover word1 (?sz35 word1 a b aa ba word2 y cap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> cte_wp_at ((=) cap) (aa, ba) s \<and> is_untyped_cap cap\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s; is_aligned word1 page_bits\<rbrakk> \<Longrightarrow> word_size_bits \<le> page_bits
 2. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s; is_aligned word1 page_bits\<rbrakk> \<Longrightarrow> page_bits \<le> word_bits
 3. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s; is_aligned word1 page_bits\<rbrakk> \<Longrightarrow> word1 && ~~ mask page_bits = word1
 4. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s; is_aligned word1 page_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- modify (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits});
modify (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1})
od \<lbrace>\<lambda>y sa. \<forall>cap. cte_wp_at ((=) cap) (aa, ba) sa \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y cap)) sa \<and> pred_tcb_at proj Q t sa \<and> range_cover word1 (?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y cap) (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> invs sa \<and> cte_wp_at ((=) cap) (aa, ba) sa \<and> is_untyped_cap cap\<rbrace>
flex-flex pairs:
\<lambda>word1 a b aa ba word2 s y sa. ?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y \<equiv>\<^sup>? \<lambda>word1 a b aa ba word2 s y sa. ?sz35 word1 a b aa ba word2 y proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s; is_aligned word1 12\<rbrakk> \<Longrightarrow> word1 && ~~ mask 12 = word1
 2. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s; is_aligned word1 page_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- modify (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits});
modify (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1})
od \<lbrace>\<lambda>y sa. \<forall>cap. cte_wp_at ((=) cap) (aa, ba) sa \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y cap)) sa \<and> pred_tcb_at proj Q t sa \<and> range_cover word1 (?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y cap) (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> invs sa \<and> cte_wp_at ((=) cap) (aa, ba) sa \<and> is_untyped_cap cap\<rbrace>
flex-flex pairs:
\<lambda>word1 a b aa ba word2 s y sa. ?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y \<equiv>\<^sup>? \<lambda>word1 a b aa ba word2 s y sa. ?sz35 word1 a b aa ba word2 y proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2 s. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s; is_aligned word1 page_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- modify (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits});
modify (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1})
od \<lbrace>\<lambda>y sa. \<forall>cap. cte_wp_at ((=) cap) (aa, ba) sa \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y cap)) sa \<and> pred_tcb_at proj Q t sa \<and> range_cover word1 (?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y cap) (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> invs sa \<and> cte_wp_at ((=) cap) (aa, ba) sa \<and> is_untyped_cap cap\<rbrace>
flex-flex pairs:
\<lambda>word1 a b aa ba word2 s y sa. ?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y \<equiv>\<^sup>? \<lambda>word1 a b aa ba word2 s y sa. ?sz35 word1 a b aa ba word2 y proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2 s sa. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; pred_tcb_at proj Q t s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> invs s \<and> valid_aci (MakePool word1 (a, b) (aa, ba) word2) s; is_aligned word1 page_bits; s = sa\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (aa, ba) (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<longrightarrow> word2 && mask local.asid_low_bits = 0 \<longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 () cap)) (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> pred_tcb_at proj Q t (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> range_cover word1 (?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 () cap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> invs (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> cte_wp_at ((=) cap) (aa, ba) (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> is_untyped_cap cap
flex-flex pairs:
\<lambda>word1 a b aa ba word2 s y sa. ?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y \<equiv>\<^sup>? \<lambda>word1 a b aa ba word2 s y sa. ?sz35 word1 a b aa ba word2 y proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 page_bits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 && ~~ mask page_bits \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ page_bits - 1; word2 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz85 word1 a b aa ba word2 sa word1 (?a85 word1 a b aa ba word2 sa) (?b85 word1 a b aa ba word2 sa) aa ba word2 () cap)) (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> (word1 && ~~ mask page_bits \<le> t \<longrightarrow> \<not> t \<le> word1 + 2 ^ page_bits - 1) \<and> range_cover word1 (?sz85 word1 a b aa ba word2 sa word1 (?a85 word1 a b aa ba word2 sa) (?b85 word1 a b aa ba word2 sa) aa ba word2 () cap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> invs (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> is_untyped_cap cap
flex-flex pairs:
\<lambda>word1 a b aa ba word2 s y sa. ?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y \<equiv>\<^sup>? \<lambda>word1 a b aa ba word2 s y sa. ?sz35 word1 a b aa ba word2 y proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 page_bits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 && ~~ mask page_bits \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ page_bits - 1; word2 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> page_bits \<le> LENGTH(32)
 2. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 page_bits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 && ~~ mask page_bits \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ page_bits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ page_bits} = {word1..word1 + 2 ^ page_bits - 1}\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz85 word1 a b aa ba word2 sa word1 (?a85 word1 a b aa ba word2 sa) (?b85 word1 a b aa ba word2 sa) aa ba word2 () cap)) (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> (word1 && ~~ mask page_bits \<le> t \<longrightarrow> \<not> t \<le> word1 + 2 ^ page_bits - 1) \<and> range_cover word1 (?sz85 word1 a b aa ba word2 sa word1 (?a85 word1 a b aa ba word2 sa) (?b85 word1 a b aa ba word2 sa) aa ba word2 () cap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> invs (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> is_untyped_cap cap
flex-flex pairs:
\<lambda>word1 a b aa ba word2 s y sa. ?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y \<equiv>\<^sup>? \<lambda>word1 a b aa ba word2 s y sa. ?sz35 word1 a b aa ba word2 y proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 page_bits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 && ~~ mask page_bits \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ page_bits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ page_bits} = {word1..word1 + 2 ^ page_bits - 1}\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz85 word1 a b aa ba word2 sa word1 (?a85 word1 a b aa ba word2 sa) (?b85 word1 a b aa ba word2 sa) aa ba word2 () cap)) (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> (word1 && ~~ mask page_bits \<le> t \<longrightarrow> \<not> t \<le> word1 + 2 ^ page_bits - 1) \<and> range_cover word1 (?sz85 word1 a b aa ba word2 sa word1 (?a85 word1 a b aa ba word2 sa) (?b85 word1 a b aa ba word2 sa) aa ba word2 () cap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> invs (detype {word1 && ~~ mask page_bits..word1 + 2 ^ page_bits - 1} (clear_um {word1 + word_of_nat k |k. k < 2 ^ page_bits} sa)) \<and> is_untyped_cap cap
flex-flex pairs:
\<lambda>word1 a b aa ba word2 s y sa. ?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y \<equiv>\<^sup>? \<lambda>word1 a b aa ba word2 s y sa. ?sz35 word1 a b aa ba word2 y proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz85 word1 a b aa ba word2 sa word1 (?a85 word1 a b aa ba word2 sa) (?b85 word1 a b aa ba word2 sa) aa ba word2 () cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> (word1 \<le> t \<longrightarrow> \<not> t \<le> word1 + 2 ^ pageBits - 1) \<and> range_cover word1 (?sz85 word1 a b aa ba word2 sa word1 (?a85 word1 a b aa ba word2 sa) (?b85 word1 a b aa ba word2 sa) aa ba word2 () cap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap
flex-flex pairs:
\<lambda>word1 a b aa ba word2 s y sa. ?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y \<equiv>\<^sup>? \<lambda>word1 a b aa ba word2 s y sa. ?sz35 word1 a b aa ba word2 y proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz85 word1 a b aa ba word2 sa word1 (?a85 word1 a b aa ba word2 sa) (?b85 word1 a b aa ba word2 sa) aa ba word2 () cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa)
 2. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> (word1 \<le> t \<longrightarrow> \<not> t \<le> word1 + 2 ^ pageBits - 1) \<and> range_cover word1 (?sz85 word1 a b aa ba word2 sa word1 (?a85 word1 a b aa ba word2 sa) (?b85 word1 a b aa ba word2 sa) aa ba word2 () cap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap
flex-flex pairs:
\<lambda>word1 a b aa ba word2 s y sa. ?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y \<equiv>\<^sup>? \<lambda>word1 a b aa ba word2 s y sa. ?sz35 word1 a b aa ba word2 y proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area word1 (?sz85 word1 a b aa ba word2 sa word1 (?a85 word1 a b aa ba word2 sa) (?b85 word1 a b aa ba word2 sa) aa ba word2 () (UntypedCap False word1 pageBits idx))) (detype {word1..word1 + 2 ^ pageBits - 1} sa)
 2. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> (word1 \<le> t \<longrightarrow> \<not> t \<le> word1 + 2 ^ pageBits - 1) \<and> range_cover word1 (?sz85 word1 a b aa ba word2 sa word1 (?a85 word1 a b aa ba word2 sa) (?b85 word1 a b aa ba word2 sa) aa ba word2 () cap) (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap
flex-flex pairs:
\<lambda>word1 a b aa ba word2 s y sa. ?sz85 word1 a b aa ba word2 s word1 (?a85 word1 a b aa ba word2 s) (?b85 word1 a b aa ba word2 s) aa ba word2 y \<equiv>\<^sup>? \<lambda>word1 a b aa ba word2 s y sa. ?sz35 word1 a b aa ba word2 y proof (prove)
goal (4 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> sa \<turnstile> UntypedCap (?dev121 word1 a b aa ba word2 sa idx) word1 pageBits (?idx121 word1 a b aa ba word2 sa idx)
 2. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> pspace_aligned sa
 3. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> valid_objs sa
 4. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> (word1 \<le> t \<longrightarrow> \<not> t \<le> word1 + 2 ^ pageBits - 1) \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (5 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> caps_of_state sa (?p125 word1 a b aa ba word2 sa idx) = Some (UntypedCap (?dev121 word1 a b aa ba word2 sa idx) word1 pageBits (?idx121 word1 a b aa ba word2 sa idx))
 2. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> valid_objs sa
 3. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> pspace_aligned sa
 4. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> valid_objs sa
 5. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> (word1 \<le> t \<longrightarrow> \<not> t \<le> word1 + 2 ^ pageBits - 1) \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (4 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> valid_objs sa
 2. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> pspace_aligned sa
 3. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> valid_objs sa
 4. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> (word1 \<le> t \<longrightarrow> \<not> t \<le> word1 + 2 ^ pageBits - 1) \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> (word1 \<le> t \<longrightarrow> \<not> t \<le> word1 + 2 ^ pageBits - 1) \<and> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> word1 \<le> t \<longrightarrow> \<not> t \<le> word1 + 2 ^ pageBits - 1
 2. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (4 subgoals):
 1. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> if_live_then_nonz_cap sa
 2. \<And>word1 a b aa ba word2 sa cap st. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; (Not \<circ> inactive and Not \<circ> idle) st\<rbrakk> \<Longrightarrow> \<not> halted st
 3. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; ex_nonz_cap_to t sa\<rbrakk> \<Longrightarrow> word1 \<le> t \<longrightarrow> \<not> t \<le> word1 + 2 ^ pageBits - 1
 4. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 sa cap st. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; (Not \<circ> inactive and Not \<circ> idle) st\<rbrakk> \<Longrightarrow> \<not> halted st
 2. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; ex_nonz_cap_to t sa\<rbrakk> \<Longrightarrow> word1 \<le> t \<longrightarrow> \<not> t \<le> word1 + 2 ^ pageBits - 1
 3. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; ex_nonz_cap_to t sa\<rbrakk> \<Longrightarrow> word1 \<le> t \<longrightarrow> \<not> t \<le> word1 + 2 ^ pageBits - 1
 2. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 sa cap ab bb. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; cte_wp_at (\<lambda>c. t \<in> zobj_refs c) (ab, bb) sa; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 sa cap ab bb. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; cte_wp_at (\<lambda>c. t \<in> zobj_refs c) (ab, bb) sa; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; untyped_children_in_mdb sa\<rbrakk> \<Longrightarrow> False
 2. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 sa ab bb idx capa. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; untyped_children_in_mdb sa; caps_of_state sa (ab, bb) = Some capa; t \<in> zobj_refs capa\<rbrakk> \<Longrightarrow> False
 2. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (6 subgoals):
 1. \<And>word1 a b aa ba word2 sa ab bb idx capa. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; caps_of_state sa (ab, bb) = Some capa; t \<in> zobj_refs capa\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap156 word1 a b aa ba word2 sa ab bb idx capa)) (aa, ba) sa
 2. \<And>word1 a b aa ba word2 sa ab bb idx capa. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; caps_of_state sa (ab, bb) = Some capa; t \<in> zobj_refs capa\<rbrakk> \<Longrightarrow> is_untyped_cap (?cap156 word1 a b aa ba word2 sa ab bb idx capa)
 3. \<And>word1 a b aa ba word2 sa ab bb idx capa. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; caps_of_state sa (ab, bb) = Some capa; t \<in> zobj_refs capa\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. ?ta159 word1 a b aa ba word2 sa ab bb idx capa \<in> zobj_refs c) (?ptr'156 word1 a b aa ba word2 sa ab bb idx capa) sa
 4. \<And>word1 a b aa ba word2 sa ab bb idx capa cap'. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; caps_of_state sa (ab, bb) = Some capa; t \<in> zobj_refs capa; cte_wp_at ((=) cap') (?ptr'156 word1 a b aa ba word2 sa ab bb idx capa) sa; ?ta159 word1 a b aa ba word2 sa ab bb idx capa \<in> zobj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (?cap156 word1 a b aa ba word2 sa ab bb idx capa) \<noteq> {}
 5. \<And>word1 a b aa ba word2 sa ab bb idx capa. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; caps_of_state sa (ab, bb) = Some capa; t \<in> zobj_refs capa; ?ptr'156 word1 a b aa ba word2 sa ab bb idx capa \<in> descendants_of (aa, ba) (cdt sa)\<rbrakk> \<Longrightarrow> False
 6. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (4 subgoals):
 1. \<And>word1 a b aa ba word2 sa ab bb idx capa. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; caps_of_state sa (ab, bb) = Some capa; t \<in> zobj_refs capa\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state sa (?ptr'156 word1 a b aa ba word2 sa ab bb idx capa) = Some cap \<and> ?ta159 word1 a b aa ba word2 sa ab bb idx capa \<in> zobj_refs cap
 2. \<And>word1 a b aa ba word2 sa ab bb idx capa cap'. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; caps_of_state sa (ab, bb) = Some capa; t \<in> zobj_refs capa; cte_wp_at ((=) cap') (?ptr'156 word1 a b aa ba word2 sa ab bb idx capa) sa; ?ta159 word1 a b aa ba word2 sa ab bb idx capa \<in> zobj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (UntypedCap False word1 pageBits idx) \<noteq> {}
 3. \<And>word1 a b aa ba word2 sa ab bb idx capa. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; caps_of_state sa (ab, bb) = Some capa; t \<in> zobj_refs capa; ?ptr'156 word1 a b aa ba word2 sa ab bb idx capa \<in> descendants_of (aa, ba) (cdt sa)\<rbrakk> \<Longrightarrow> False
 4. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 sa ab bb idx capa cap'. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; caps_of_state sa (ab, bb) = Some capa; t \<in> zobj_refs capa; cte_wp_at ((=) cap') (ab, bb) sa; t \<in> zobj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (UntypedCap False word1 pageBits idx) \<noteq> {}
 2. \<And>word1 a b aa ba word2 sa ab bb idx capa. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; caps_of_state sa (ab, bb) = Some capa; t \<in> zobj_refs capa; (ab, bb) \<in> descendants_of (aa, ba) (cdt sa)\<rbrakk> \<Longrightarrow> False
 3. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (3 subgoals):
 1. \<And>word1 a b aa ba word2 sa ab bb idx capa cap'. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; caps_of_state sa (ab, bb) = Some capa; cte_wp_at ((=) cap') (ab, bb) sa; t \<in> obj_refs capa; \<not> is_zombie capa; t \<in> obj_refs cap'; \<not> is_zombie cap'; obj_refs cap' \<inter> {word1..word1 + 2 ^ pageBits - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>word1 a b aa ba word2 sa ab bb idx capa. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; caps_of_state sa (ab, bb) = Some capa; t \<in> zobj_refs capa; (ab, bb) \<in> descendants_of (aa, ba) (cdt sa)\<rbrakk> \<Longrightarrow> False
 3. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 sa ab bb idx capa. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; word1 \<le> t; t \<le> word1 + 2 ^ pageBits - 1; caps_of_state sa (ab, bb) = Some capa; t \<in> zobj_refs capa; (ab, bb) \<in> descendants_of (aa, ba) (cdt sa)\<rbrakk> \<Longrightarrow> False
 2. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2 sa cap. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cte_wp_at (\<lambda>c. c = NullCap) (a, b) sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False word1 pageBits idx) (aa, ba) sa; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; cte_wp_at ((=) cap) (aa, ba) sa; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> range_cover word1 pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> descendants_range_in (untyped_range cap) (aa, ba) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> is_untyped_cap cap proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> range_cover word1 pageBits pageBits (Suc 0) \<and> pspace_no_overlap (up_aligned_area word1 pageBits) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} 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; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) (?ptr260 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; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> is_untyped_cap (UntypedCap False word1 pageBits idx)
 3. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}\<rbrakk> \<Longrightarrow> descendants_range (UntypedCap False word1 pageBits idx) (?ptr260 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; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; (invs and untyped_children_in_mdb) (detype (untyped_range (UntypedCap False word1 pageBits idx)) (clear_um (untyped_range (UntypedCap False word1 pageBits idx)) sa))\<rbrakk> \<Longrightarrow> range_cover word1 pageBits pageBits (Suc 0) \<and> pspace_no_overlap (up_aligned_area word1 pageBits) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; caps_of_state sa (a, b) = Some NullCap; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; invs (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> untyped_children_in_mdb (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa))\<rbrakk> \<Longrightarrow> range_cover word1 pageBits pageBits (Suc 0) \<and> pspace_no_overlap (up_aligned_area word1 pageBits) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; caps_of_state sa (aa, ba) = Some (UntypedCap False word1 pageBits idx); word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; invs (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> untyped_children_in_mdb (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa))\<rbrakk> \<Longrightarrow> range_cover word1 pageBits pageBits (Suc 0) \<and> pspace_no_overlap (up_aligned_area word1 pageBits) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) proof (prove)
goal (1 subgoal):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; invs (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> untyped_children_in_mdb (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)); sa \<turnstile> UntypedCap False word1 pageBits idx\<rbrakk> \<Longrightarrow> range_cover word1 pageBits pageBits (Suc 0) \<and> pspace_no_overlap (up_aligned_area word1 pageBits) (detype {word1..word1 + 2 ^ pageBits - 1} sa) \<and> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} 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; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; invs (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> untyped_children_in_mdb (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)); sa \<turnstile> UntypedCap False word1 pageBits idx\<rbrakk> \<Longrightarrow> range_cover word1 pageBits pageBits (Suc 0)
 2. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; invs (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> untyped_children_in_mdb (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)); sa \<turnstile> UntypedCap False word1 pageBits idx\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area word1 pageBits) (detype {word1..word1 + 2 ^ pageBits - 1} sa)
 3. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; invs (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> untyped_children_in_mdb (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)); sa \<turnstile> UntypedCap False word1 pageBits idx\<rbrakk> \<Longrightarrow> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) proof (prove)
goal (2 subgoals):
 1. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; invs (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> untyped_children_in_mdb (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)); sa \<turnstile> UntypedCap False word1 pageBits idx\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area word1 pageBits) (detype {word1..word1 + 2 ^ pageBits - 1} sa)
 2. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; invs (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> untyped_children_in_mdb (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)); sa \<turnstile> UntypedCap False word1 pageBits idx\<rbrakk> \<Longrightarrow> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} 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; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; invs (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> untyped_children_in_mdb (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa))\<rbrakk> \<Longrightarrow> pspace_aligned sa
 2. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; invs (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> untyped_children_in_mdb (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa))\<rbrakk> \<Longrightarrow> valid_objs sa
 3. \<And>word1 a b aa ba word2 sa idx. \<lbrakk>aci = MakePool word1 (a, b) (aa, ba) word2; is_aligned word1 pageBits; pred_tcb_at proj Q t sa; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t sa; ct_active sa; invs sa; cap_table_at (length b) a sa; ex_cte_cap_wp_to is_cnode_cap (a, b) sa; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt sa) = {}; is_aligned word2 local.asid_low_bits; word2 < 2 ^ local.asid_bits; asid_table sa (asid_high_bits_of word2) = None; word1 \<le> aa \<longrightarrow> \<not> aa \<le> word1 + 2 ^ pageBits - 1; word2 && mask local.asid_low_bits = 0; {word1 + word_of_nat k |k. k < 2 ^ pageBits} = {word1..word1 + 2 ^ pageBits - 1}; invs (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)) \<and> untyped_children_in_mdb (detype {word1..word1 + 2 ^ pageBits - 1} (clear_um {word1..word1 + 2 ^ pageBits - 1} sa)); sa \<turnstile> UntypedCap False word1 pageBits idx\<rbrakk> \<Longrightarrow> invs (clear_um {word1..word1 + 2 ^ pageBits - 1} (detype {word1..word1 + 2 ^ pageBits - 1} sa)) proof (prove)
goal:
No subgoals!