theory Arch_R

lemma performASIDControlInvocation_invs' [wp]:
  "\<lbrace>invs' and ct_active' and valid_aci' aci\<rbrace>
  performASIDControlInvocation aci \<lbrace>\<lambda>y. invs'\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: performASIDControlInvocation_def valid_aci'_def
    placeNewObject_def2 cte_wp_at_ctes_of
    split: asidcontrol_invocation.splits) apply (rename_tac w1 w2 w3 w4 cte ctea idx) apply (case_tac ctea) apply (clarsimp) apply (frule ctes_of_valid_cap') apply fastforce apply (rule hoare_pre) apply (wp hoare_vcg_const_imp_lift) apply (strengthen invs_asid_table_strengthen') apply (wp cteInsert_simple_invs) apply (wp createObjects'_wp_subst[OF
                createObjects_no_cte_invs [where sz = pageBits and ty="Inl (KOArch (KOASIDPool pool))" for pool]]
                createObjects_orig_cte_wp_at'[where sz = pageBits]  hoare_vcg_const_imp_lift
         |simp add: makeObjectKO_def projectKOs asid_pool_typ_at_ext' valid_cap'_def cong: rev_conj_cong
         |strengthen safe_parent_strg'[where idx= "2^ pageBits"])+ apply (rule hoare_vcg_conj_lift) apply (rule descendants_of'_helper) apply (wp createObjects_null_filter'
                  [where sz = pageBits and ty="Inl (KOArch (KOASIDPool ap))" for ap]
                 createObjects_valid_pspace'
                  [where sz = pageBits and ty="Inl (KOArch (KOASIDPool ap))" for ap]
          | simp add: makeObjectKO_def projectKOs asid_pool_typ_at_ext' valid_cap'_def
                cong: rev_conj_cong)+ apply (simp add: objBits_simps archObjSize_def valid_cap'_def capAligned_def range_cover_full) apply (wp  createObjects'_wp_subst[OF createObjects_ex_cte_cap_to[where sz = pageBits]]
                 createObjects_orig_cte_wp_at'[where sz = pageBits]
                 hoare_vcg_const_imp_lift
         |simp add: makeObjectKO_def projectKOs asid_pool_typ_at_ext' valid_cap'_def cong: rev_conj_cong
         |strengthen safe_parent_strg'[where idx = "2^ pageBits"])+ apply (simp add:asid_pool_typ_at_ext'[symmetric]) apply (wp createObject_typ_at') apply (simp add: objBits_simps archObjSize_def valid_cap'_def
         capAligned_def range_cover_full makeObjectKO_def
         projectKOs asid_pool_typ_at_ext'
         cong: rev_conj_cong) apply (clarsimp simp:conj_comms
                         descendants_of_null_filter'
      | strengthen invs_pspace_aligned' invs_pspace_distinct'
          invs_pspace_aligned' invs_valid_pspace')+ apply (wp updateFreeIndex_forward_invs'
           updateFreeIndex_cte_wp_at
           updateFreeIndex_pspace_no_overlap'
           updateFreeIndex_caps_no_overlap''
           updateFreeIndex_descendants_of2
           updateFreeIndex_caps_overlap_reserved
           updateCap_cte_wp_at_cases hoare_weak_lift_imp
           getSlotCap_wp)+ apply (clarsimp simp:conj_comms ex_disj_distrib is_aligned_mask
           | strengthen invs_valid_pspace' invs_pspace_aligned'
                        invs_pspace_distinct' empty_descendants_range_in')+ apply (wp deleteObjects_invs'[where p="makePoolParent aci"]
            hoare_vcg_ex_lift
            deleteObjects_caps_no_overlap''[where slot="makePoolParent aci"]
            deleteObject_no_overlap
            deleteObjects_cap_to'[where p="makePoolParent aci"]
            deleteObjects_ct_active'[where cref="makePoolParent aci"]
            deleteObjects_descendants[where p="makePoolParent aci"]
            deleteObjects_cte_wp_at'
            deleteObjects_null_filter[where p="makePoolParent aci"]) apply (frule valid_capAligned) apply (clarsimp simp: invs_mdb' invs_valid_pspace' capAligned_def
                        cte_wp_at_ctes_of is_simple_cap'_def isCap_simps) apply (strengthen refl ctes_of_valid_cap'[mk_strg I E]) apply (clarsimp simp: conj_comms invs_valid_objs') apply (frule_tac ptr="w1" in descendants_range_caps_no_overlapI'[where sz = pageBits]) apply (fastforce simp: cte_wp_at_ctes_of) apply (simp add:empty_descendants_range_in') apply (frule(1) if_unsafe_then_capD'[OF _ invs_unsafe_then_cap',rotated]) apply (fastforce simp:cte_wp_at_ctes_of) apply (drule ex_cte_not_in_untyped_range[rotated -2]) apply (simp add:invs_valid_global')+ apply (drule ex_cte_not_in_untyped_range[rotated -2]) apply (simp add:invs_valid_global')+ apply (subgoal_tac "is_aligned (2 ^ pageBits) minUntypedSizeBits") prefer 2 apply (rule is_aligned_weaken) apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) apply (simp add: pageBits_def minUntypedSizeBits_def) apply (frule_tac cte="CTE (capability.UntypedCap False a b c) m" for a b c m in valid_global_refsD', clarsimp) apply (simp add: Int_commute) by (auto simp:empty_descendants_range_in' objBits_simps max_free_index_def
                    archObjSize_def asid_low_bits_def word_bits_def pageBits_def
                    range_cover_full descendants_range'_def2 is_aligned_mask
                    null_filter_descendants_of'[OF null_filter_simp']
                    valid_cap_simps' mask_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active' and valid_aci' aci\<rbrace> performASIDControlInvocation aci \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and ct_active' and valid_aci' aci) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> performASIDControlInvocation aci \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x3 x4 cte ctea idx. \<lbrakk>aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; invs' s; ct_active' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some ctea; cteCap ctea = capability.UntypedCap False x1 pageBits idx; x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- deleteObjects x1 pageBits;
pcap <- getSlotCap x3;
y <- updateFreeIndex x3 (max_free_index (capBlockSize pcap));
y <- createObjects' x1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0;
y <- cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap x1 x4)) x3 x2;
y <- assert (x4 && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of x4) \<mapsto> x1)) (ksArchState s)\<rparr>)
od \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s w1 w2 w3 w4 cte ctea idx. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some ctea; cteCap ctea = capability.UntypedCap False w1 pageBits idx; w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- deleteObjects w1 pageBits;
pcap <- getSlotCap w3;
y <- updateFreeIndex w3 (max_free_index (capBlockSize pcap));
y <- createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0;
y <- cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) w3 w2;
y <- assert (w4 && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of w4) \<mapsto> w1)) (ksArchState s)\<rparr>)
od \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s w1 w2 w3 w4 cte ctea idx x1 x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some ctea; cteCap ctea = capability.UntypedCap False w1 pageBits idx; w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- deleteObjects w1 pageBits;
pcap <- getSlotCap w3;
y <- updateFreeIndex w3 (max_free_index (capBlockSize pcap));
y <- createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0;
y <- cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) w3 w2;
y <- assert (w4 && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of w4) \<mapsto> w1)) (ksArchState s)\<rparr>)
od \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- deleteObjects w1 pageBits;
pcap <- getSlotCap w3;
y <- updateFreeIndex w3 (max_free_index (capBlockSize pcap));
y <- createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0;
y <- cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) w3 w2;
y <- assert (w4 && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of w4) \<mapsto> w1)) (ksArchState s)\<rparr>)
od \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> valid_objs' s
 2. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- deleteObjects w1 pageBits;
pcap <- getSlotCap w3;
y <- updateFreeIndex w3 (max_free_index (capBlockSize pcap));
y <- createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0;
y <- cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) w3 w2;
y <- assert (w4 && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of w4) \<mapsto> w1)) (ksArchState s)\<rparr>)
od \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- deleteObjects w1 pageBits;
pcap <- getSlotCap w3;
y <- updateFreeIndex w3 (max_free_index (capBlockSize pcap));
y <- createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0;
y <- cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) w3 w2;
y <- assert (w4 && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of w4) \<mapsto> w1)) (ksArchState s)\<rparr>)
od \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 s w1 w2 w3 w4 cte idx x2\<rbrace> do y <- deleteObjects w1 pageBits;
pcap <- getSlotCap w3;
y <- updateFreeIndex w3 (max_free_index (capBlockSize pcap));
y <- createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0;
y <- cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) w3 w2;
y <- assert (w4 && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of w4) \<mapsto> w1)) (ksArchState s)\<rparr>)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q41 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (6 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2 y pcap ya yb. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; w4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 s w1 w2 w3 w4 cte idx x2 y pcap ya yb\<rbrace> cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) w3 w2 \<lbrace>\<lambda>rv s. invs' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. ((armKSASIDTable \<circ> ksArchState) s)(UCAST(7 \<rightarrow> 32) (asid_high_bits_of w4) \<mapsto> w1)) (ksArchState s)\<rparr>)\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 y pcap ya. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B47 s w1 w2 w3 w4 cte idx x2 y pcap ya\<rbrace> createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>yb sa. w4 && mask local.asid_low_bits = 0 \<longrightarrow> ?Q56 s w1 w2 w3 w4 cte idx x2 y pcap ya yb sa\<rbrace>
 3. \<And>s w1 w2 w3 w4 cte idx x2 y pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y pcap\<rbrace> updateFreeIndex w3 (max_free_index (capBlockSize pcap)) \<lbrace>?B47 s w1 w2 w3 w4 cte idx x2 y pcap\<rbrace>
 4. \<And>s w1 w2 w3 w4 cte idx x2 y. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2 y\<rbrace> getSlotCap w3 \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y\<rbrace>
 5. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2\<rbrace>
 6. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q41 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (6 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2 y pcap ya yb. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; w4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 s w1 w2 w3 w4 cte idx x2 y pcap ya yb\<rbrace> cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) w3 w2 \<lbrace>\<lambda>r sa. invs' sa \<and> asid_pool_at' w1 sa \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of w4) \<le> 2 ^ local.asid_high_bits - 1\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 y pcap ya. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B47 s w1 w2 w3 w4 cte idx x2 y pcap ya\<rbrace> createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>yb sa. w4 && mask local.asid_low_bits = 0 \<longrightarrow> ?Q56 s w1 w2 w3 w4 cte idx x2 y pcap ya yb sa\<rbrace>
 3. \<And>s w1 w2 w3 w4 cte idx x2 y pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y pcap\<rbrace> updateFreeIndex w3 (max_free_index (capBlockSize pcap)) \<lbrace>?B47 s w1 w2 w3 w4 cte idx x2 y pcap\<rbrace>
 4. \<And>s w1 w2 w3 w4 cte idx x2 y. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2 y\<rbrace> getSlotCap w3 \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y\<rbrace>
 5. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2\<rbrace>
 6. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q41 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (5 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2 y pcap ya. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B47 s w1 w2 w3 w4 cte idx x2 y pcap ya\<rbrace> createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>yb s. w4 && mask local.asid_low_bits = 0 \<longrightarrow> (invs' and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) w2 and valid_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) and (\<lambda>s. w3 \<noteq> w2) and (\<lambda>s. safe_parent_for' (ctes_of s) w3 (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4))) and (\<lambda>s. \<forall>irq. capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4) = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) and cte_wp_at' (\<lambda>_. True) w3 and ex_cte_cap_wp_to' (\<lambda>_. True) w2 and K (is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)))) s \<and> asid_pool_at' w1 s \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of w4) \<le> 2 ^ local.asid_high_bits - 1\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 y pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y pcap\<rbrace> updateFreeIndex w3 (max_free_index (capBlockSize pcap)) \<lbrace>?B47 s w1 w2 w3 w4 cte idx x2 y pcap\<rbrace>
 3. \<And>s w1 w2 w3 w4 cte idx x2 y. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2 y\<rbrace> getSlotCap w3 \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y\<rbrace>
 4. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2\<rbrace>
 5. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q41 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (5 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2 pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; capAligned (capability.UntypedCap False w1 pageBits idx) \<and> valid_untyped' False w1 pageBits idx s \<and> w1 \<noteq> 0 \<and> minUntypedSizeBits \<le> pageBits \<and> pageBits \<le> maxUntypedSizeBits \<and> idx \<le> 2 ^ pageBits \<and> is_aligned (word_of_nat idx) minUntypedSizeBits; w4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'129 s w1 w2 w3 w4 cte idx x2 () pcap ()\<rbrace> createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>rv s. descendants_of' w3 (ctes_of s) = {} \<and> valid_pspace' s \<and> cte_wp_at' (\<lambda>_. True) w3 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) w2 s \<and> is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> obj_at' (\<lambda>_. True) w1 s\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 y pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y pcap\<rbrace> updateFreeIndex w3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>ya sa. w4 && mask local.asid_low_bits = 0 \<longrightarrow> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> invs' sa \<and> ct_active' sa \<and> pspace_no_overlap' w1 pageBits sa \<and> w1 \<noteq> 0 \<and> {w1..(w1 && ~~ mask pageBits) + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {w1..w1 + word_of_nat (Suc 0 * 2 ^ 0 * 2 ^ objBitsKO (KOArch (KOASIDPool makeObject))) - 1} sa \<and> caps_no_overlap'' w1 pageBits sa \<and> refs_of' (KOArch (KOASIDPool makeObject)) = {} \<and> \<not> live' (KOArch (KOASIDPool makeObject)) \<and> (\<forall>pde. projectKO_opt (KOArch (KOASIDPool makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) w2 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>a. cteCap a = capability.UntypedCap False w1 pageBits (2 ^ pageBits)) w3 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> ?P'129 s w1 w2 w3 w4 cte idx x2 y pcap ya sa\<rbrace>
 3. \<And>s w1 w2 w3 w4 cte idx x2 y. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2 y\<rbrace> getSlotCap w3 \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y\<rbrace>
 4. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2\<rbrace>
 5. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q41 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (6 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2 pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; capAligned (capability.UntypedCap False w1 pageBits idx) \<and> valid_untyped' False w1 pageBits idx s \<and> w1 \<noteq> 0 \<and> minUntypedSizeBits \<le> pageBits \<and> pageBits \<le> maxUntypedSizeBits \<and> idx \<le> 2 ^ pageBits \<and> is_aligned (word_of_nat idx) minUntypedSizeBits; w4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P136 s w1 w2 w3 w4 cte idx x2 () pcap ()\<rbrace> createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>rv s. descendants_of' w3 (ctes_of s) = {}\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; capAligned (capability.UntypedCap False w1 pageBits idx) \<and> valid_untyped' False w1 pageBits idx s \<and> w1 \<noteq> 0 \<and> minUntypedSizeBits \<le> pageBits \<and> pageBits \<le> maxUntypedSizeBits \<and> idx \<le> 2 ^ pageBits \<and> is_aligned (word_of_nat idx) minUntypedSizeBits; w4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'135 s w1 w2 w3 w4 cte idx x2 () pcap ()\<rbrace> createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>rv s. valid_pspace' s \<and> cte_wp_at' (\<lambda>_. True) w3 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) w2 s \<and> is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> obj_at' (\<lambda>_. True) w1 s\<rbrace>
 3. \<And>s w1 w2 w3 w4 cte idx x2 y pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y pcap\<rbrace> updateFreeIndex w3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>ya sa. w4 && mask local.asid_low_bits = 0 \<longrightarrow> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> invs' sa \<and> ct_active' sa \<and> pspace_no_overlap' w1 pageBits sa \<and> w1 \<noteq> 0 \<and> {w1..(w1 && ~~ mask pageBits) + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {w1..w1 + word_of_nat (Suc 0 * 2 ^ 0 * 2 ^ objBitsKO (KOArch (KOASIDPool makeObject))) - 1} sa \<and> caps_no_overlap'' w1 pageBits sa \<and> refs_of' (KOArch (KOASIDPool makeObject)) = {} \<and> \<not> live' (KOArch (KOASIDPool makeObject)) \<and> (\<forall>pde. projectKO_opt (KOArch (KOASIDPool makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) w2 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>a. cteCap a = capability.UntypedCap False w1 pageBits (2 ^ pageBits)) w3 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> ?P136 s w1 w2 w3 w4 cte idx x2 y pcap ya sa \<and> ?P'135 s w1 w2 w3 w4 cte idx x2 y pcap ya sa\<rbrace>
 4. \<And>s w1 w2 w3 w4 cte idx x2 y. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2 y\<rbrace> getSlotCap w3 \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y\<rbrace>
 5. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2\<rbrace>
 6. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q41 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (6 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2 pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; capAligned (capability.UntypedCap False w1 pageBits idx) \<and> valid_untyped' False w1 pageBits idx s \<and> w1 \<noteq> 0 \<and> minUntypedSizeBits \<le> pageBits \<and> pageBits \<le> maxUntypedSizeBits \<and> idx \<le> 2 ^ pageBits \<and> is_aligned (word_of_nat idx) minUntypedSizeBits; w4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P136 s w1 w2 w3 w4 cte idx x2 () pcap ()\<rbrace> createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>rv s. descendants_of' w3 (null_filter' (ctes_of s)) = {}\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; capAligned (capability.UntypedCap False w1 pageBits idx) \<and> valid_untyped' False w1 pageBits idx s \<and> w1 \<noteq> 0 \<and> minUntypedSizeBits \<le> pageBits \<and> pageBits \<le> maxUntypedSizeBits \<and> idx \<le> 2 ^ pageBits \<and> is_aligned (word_of_nat idx) minUntypedSizeBits; w4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'135 s w1 w2 w3 w4 cte idx x2 () pcap ()\<rbrace> createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>rv s. valid_pspace' s \<and> cte_wp_at' (\<lambda>_. True) w3 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) w2 s \<and> is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> obj_at' (\<lambda>_. True) w1 s\<rbrace>
 3. \<And>s w1 w2 w3 w4 cte idx x2 y pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y pcap\<rbrace> updateFreeIndex w3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>ya sa. w4 && mask local.asid_low_bits = 0 \<longrightarrow> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> invs' sa \<and> ct_active' sa \<and> pspace_no_overlap' w1 pageBits sa \<and> w1 \<noteq> 0 \<and> {w1..(w1 && ~~ mask pageBits) + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {w1..w1 + word_of_nat (Suc 0 * 2 ^ 0 * 2 ^ objBitsKO (KOArch (KOASIDPool makeObject))) - 1} sa \<and> caps_no_overlap'' w1 pageBits sa \<and> refs_of' (KOArch (KOASIDPool makeObject)) = {} \<and> \<not> live' (KOArch (KOASIDPool makeObject)) \<and> (\<forall>pde. projectKO_opt (KOArch (KOASIDPool makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) w2 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>a. cteCap a = capability.UntypedCap False w1 pageBits (2 ^ pageBits)) w3 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> ?P136 s w1 w2 w3 w4 cte idx x2 y pcap ya sa \<and> ?P'135 s w1 w2 w3 w4 cte idx x2 y pcap ya sa\<rbrace>
 4. \<And>s w1 w2 w3 w4 cte idx x2 y. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2 y\<rbrace> getSlotCap w3 \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y\<rbrace>
 5. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2\<rbrace>
 6. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q41 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (6 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; capAligned (capability.UntypedCap False w1 pageBits idx) \<and> valid_untyped' False w1 pageBits idx s \<and> w1 \<noteq> 0 \<and> minUntypedSizeBits \<le> pageBits \<and> pageBits \<le> maxUntypedSizeBits \<and> idx \<le> 2 ^ pageBits \<and> is_aligned (word_of_nat idx) minUntypedSizeBits; w4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject))) (Suc 0)
 2. \<And>s w1 w2 w3 w4 cte idx x2 pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; capAligned (capability.UntypedCap False w1 pageBits idx) \<and> valid_untyped' False w1 pageBits idx s \<and> w1 \<noteq> 0 \<and> minUntypedSizeBits \<le> pageBits \<and> pageBits \<le> maxUntypedSizeBits \<and> idx \<le> 2 ^ pageBits \<and> is_aligned (word_of_nat idx) minUntypedSizeBits; w4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'154 s w1 w2 w3 w4 cte idx x2 () pcap ()\<rbrace> createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>_. True) w3 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) w2 s \<and> is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> obj_at' (\<lambda>_. True) w1 s\<rbrace>
 3. \<And>s w1 w2 w3 w4 cte idx x2 y pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y pcap\<rbrace> updateFreeIndex w3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>ya sa. w4 && mask local.asid_low_bits = 0 \<longrightarrow> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> invs' sa \<and> ct_active' sa \<and> pspace_no_overlap' w1 pageBits sa \<and> w1 \<noteq> 0 \<and> {w1..(w1 && ~~ mask pageBits) + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {w1..w1 + word_of_nat (Suc 0 * 2 ^ 0 * 2 ^ objBitsKO (KOArch (KOASIDPool makeObject))) - 1} sa \<and> caps_no_overlap'' w1 pageBits sa \<and> refs_of' (KOArch (KOASIDPool makeObject)) = {} \<and> \<not> live' (KOArch (KOASIDPool makeObject)) \<and> (\<forall>pde. projectKO_opt (KOArch (KOASIDPool makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) w2 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>a. cteCap a = capability.UntypedCap False w1 pageBits (2 ^ pageBits)) w3 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> (descendants_of' w3 (null_filter' (ctes_of sa)) = {} \<and> makeObjectKO (?dev150 s w1 w2 w3 w4 cte idx x2 y pcap ya) (Inl (KOArch (KOASIDPool (?ap149 s w1 w2 w3 w4 cte idx x2 y pcap ya)))) = Some (KOArch (KOASIDPool makeObject)) \<and> range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> (pspace_no_overlap' w1 pageBits sa \<and> valid_pspace' sa \<and> caps_no_overlap'' w1 pageBits sa \<and> caps_overlap_reserved' {w1..w1 + word_of_nat (Suc 0 * 2 ^ 0 * 2 ^ objBitsKO (KOArch (KOASIDPool makeObject))) - 1} sa \<and> w1 \<noteq> 0) \<and> ?P'154 s w1 w2 w3 w4 cte idx x2 y pcap ya sa\<rbrace>
 4. \<And>s w1 w2 w3 w4 cte idx x2 y. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2 y\<rbrace> getSlotCap w3 \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y\<rbrace>
 5. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2\<rbrace>
 6. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q41 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (5 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2 pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; capAligned (capability.UntypedCap False w1 pageBits idx) \<and> valid_untyped' False w1 pageBits idx s \<and> w1 \<noteq> 0 \<and> minUntypedSizeBits \<le> pageBits \<and> pageBits \<le> maxUntypedSizeBits \<and> idx \<le> 2 ^ pageBits \<and> is_aligned (word_of_nat idx) minUntypedSizeBits; w4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'154 s w1 w2 w3 w4 cte idx x2 () pcap ()\<rbrace> createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>_. True) w3 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) w2 s \<and> is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> obj_at' (\<lambda>_. True) w1 s\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 y pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y pcap\<rbrace> updateFreeIndex w3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>ya sa. w4 && mask local.asid_low_bits = 0 \<longrightarrow> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> invs' sa \<and> ct_active' sa \<and> pspace_no_overlap' w1 pageBits sa \<and> w1 \<noteq> 0 \<and> {w1..(w1 && ~~ mask pageBits) + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {w1..w1 + word_of_nat (Suc 0 * 2 ^ 0 * 2 ^ objBitsKO (KOArch (KOASIDPool makeObject))) - 1} sa \<and> caps_no_overlap'' w1 pageBits sa \<and> refs_of' (KOArch (KOASIDPool makeObject)) = {} \<and> \<not> live' (KOArch (KOASIDPool makeObject)) \<and> (\<forall>pde. projectKO_opt (KOArch (KOASIDPool makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) w2 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>a. cteCap a = capability.UntypedCap False w1 pageBits (2 ^ pageBits)) w3 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> (descendants_of' w3 (null_filter' (ctes_of sa)) = {} \<and> makeObjectKO (?dev150 s w1 w2 w3 w4 cte idx x2 y pcap ya) (Inl (KOArch (KOASIDPool (?ap149 s w1 w2 w3 w4 cte idx x2 y pcap ya)))) = Some (KOArch (KOASIDPool makeObject)) \<and> range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> (pspace_no_overlap' w1 pageBits sa \<and> valid_pspace' sa \<and> caps_no_overlap'' w1 pageBits sa \<and> caps_overlap_reserved' {w1..w1 + word_of_nat (Suc 0 * 2 ^ 0 * 2 ^ objBitsKO (KOArch (KOASIDPool makeObject))) - 1} sa \<and> w1 \<noteq> 0) \<and> ?P'154 s w1 w2 w3 w4 cte idx x2 y pcap ya sa\<rbrace>
 3. \<And>s w1 w2 w3 w4 cte idx x2 y. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2 y\<rbrace> getSlotCap w3 \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y\<rbrace>
 4. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2\<rbrace>
 5. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q41 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (5 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2 pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; capAligned (capability.UntypedCap False w1 pageBits idx) \<and> valid_untyped' False w1 pageBits idx s \<and> w1 \<noteq> 0 \<and> minUntypedSizeBits \<le> pageBits \<and> pageBits \<le> maxUntypedSizeBits \<and> idx \<le> 2 ^ pageBits \<and> is_aligned (word_of_nat idx) minUntypedSizeBits; w4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'173 s w1 w2 w3 w4 cte idx x2 () pcap ()\<rbrace> createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>rv. obj_at' (\<lambda>_. True) w1\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 y pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y pcap\<rbrace> updateFreeIndex w3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>ya sa. w4 && mask local.asid_low_bits = 0 \<longrightarrow> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> invs' sa \<and> ct_active' sa \<and> pspace_no_overlap' w1 pageBits sa \<and> w1 \<noteq> 0 \<and> {w1..(w1 && ~~ mask pageBits) + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {w1..w1 + word_of_nat (Suc 0 * 2 ^ 0 * 2 ^ objBitsKO (KOArch (KOASIDPool makeObject))) - 1} sa \<and> caps_no_overlap'' w1 pageBits sa \<and> refs_of' (KOArch (KOASIDPool makeObject)) = {} \<and> \<not> live' (KOArch (KOASIDPool makeObject)) \<and> (\<forall>pde. projectKO_opt (KOArch (KOASIDPool makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) w2 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>a. cteCap a = capability.UntypedCap False w1 pageBits (2 ^ pageBits)) w3 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> (descendants_of' w3 (null_filter' (ctes_of sa)) = {} \<and> makeObjectKO (?dev150 s w1 w2 w3 w4 cte idx x2 y pcap ya) (Inl (KOArch (KOASIDPool (?ap149 s w1 w2 w3 w4 cte idx x2 y pcap ya)))) = Some (KOArch (KOASIDPool makeObject)) \<and> range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> (pspace_no_overlap' w1 pageBits sa \<and> valid_pspace' sa \<and> caps_no_overlap'' w1 pageBits sa \<and> caps_overlap_reserved' {w1..w1 + word_of_nat (Suc 0 * 2 ^ 0 * 2 ^ objBitsKO (KOArch (KOASIDPool makeObject))) - 1} sa \<and> w1 \<noteq> 0) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>a. True) w3 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> ?P'173 s w1 w2 w3 w4 cte idx x2 y pcap ya sa\<rbrace>
 3. \<And>s w1 w2 w3 w4 cte idx x2 y. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2 y\<rbrace> getSlotCap w3 \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y\<rbrace>
 4. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2\<rbrace>
 5. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q41 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (5 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2 pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; capAligned (capability.UntypedCap False w1 pageBits idx) \<and> valid_untyped' False w1 pageBits idx s \<and> w1 \<noteq> 0 \<and> minUntypedSizeBits \<le> pageBits \<and> pageBits \<le> maxUntypedSizeBits \<and> idx \<le> 2 ^ pageBits \<and> is_aligned (word_of_nat idx) minUntypedSizeBits; w4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'173 s w1 w2 w3 w4 cte idx x2 () pcap ()\<rbrace> createObjects' w1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>rv. asid_pool_at' w1\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 y pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y pcap\<rbrace> updateFreeIndex w3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>ya sa. w4 && mask local.asid_low_bits = 0 \<longrightarrow> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> invs' sa \<and> ct_active' sa \<and> pspace_no_overlap' w1 pageBits sa \<and> w1 \<noteq> 0 \<and> {w1..(w1 && ~~ mask pageBits) + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {w1..w1 + word_of_nat (Suc 0 * 2 ^ 0 * 2 ^ objBitsKO (KOArch (KOASIDPool makeObject))) - 1} sa \<and> caps_no_overlap'' w1 pageBits sa \<and> refs_of' (KOArch (KOASIDPool makeObject)) = {} \<and> \<not> live' (KOArch (KOASIDPool makeObject)) \<and> (\<forall>pde. projectKO_opt (KOArch (KOASIDPool makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) w2 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>a. cteCap a = capability.UntypedCap False w1 pageBits (2 ^ pageBits)) w3 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> (descendants_of' w3 (null_filter' (ctes_of sa)) = {} \<and> makeObjectKO (?dev150 s w1 w2 w3 w4 cte idx x2 y pcap ya) (Inl (KOArch (KOASIDPool (?ap149 s w1 w2 w3 w4 cte idx x2 y pcap ya)))) = Some (KOArch (KOASIDPool makeObject)) \<and> range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> (pspace_no_overlap' w1 pageBits sa \<and> valid_pspace' sa \<and> caps_no_overlap'' w1 pageBits sa \<and> caps_overlap_reserved' {w1..w1 + word_of_nat (Suc 0 * 2 ^ 0 * 2 ^ objBitsKO (KOArch (KOASIDPool makeObject))) - 1} sa \<and> w1 \<noteq> 0) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>a. True) w3 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> ?P'173 s w1 w2 w3 w4 cte idx x2 y pcap ya sa\<rbrace>
 3. \<And>s w1 w2 w3 w4 cte idx x2 y. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2 y\<rbrace> getSlotCap w3 \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y\<rbrace>
 4. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2\<rbrace>
 5. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q41 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (4 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2 y pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y pcap\<rbrace> updateFreeIndex w3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>ya sa. w4 && mask local.asid_low_bits = 0 \<longrightarrow> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> invs' sa \<and> ct_active' sa \<and> pspace_no_overlap' w1 pageBits sa \<and> w1 \<noteq> 0 \<and> {w1..(w1 && ~~ mask pageBits) + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {w1..w1 + word_of_nat (Suc 0 * 2 ^ 0 * 2 ^ objBitsKO (KOArch (KOASIDPool makeObject))) - 1} sa \<and> caps_no_overlap'' w1 pageBits sa \<and> refs_of' (KOArch (KOASIDPool makeObject)) = {} \<and> \<not> live' (KOArch (KOASIDPool makeObject)) \<and> (\<forall>pde. projectKO_opt (KOArch (KOASIDPool makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) w2 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> capAligned (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>a. cteCap a = capability.UntypedCap False w1 pageBits (2 ^ pageBits)) w3 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> (descendants_of' w3 (null_filter' (ctes_of sa)) = {} \<and> makeObjectKO (?dev150 s w1 w2 w3 w4 cte idx x2 y pcap ya) (Inl (KOArch (KOASIDPool (?ap149 s w1 w2 w3 w4 cte idx x2 y pcap ya)))) = Some (KOArch (KOASIDPool makeObject)) \<and> range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> (pspace_no_overlap' w1 pageBits sa \<and> valid_pspace' sa \<and> caps_no_overlap'' w1 pageBits sa \<and> caps_overlap_reserved' {w1..w1 + word_of_nat (Suc 0 * 2 ^ 0 * 2 ^ objBitsKO (KOArch (KOASIDPool makeObject))) - 1} sa \<and> w1 \<noteq> 0) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> cte_wp_at' (\<lambda>a. True) w3 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> (range_cover w1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa \<and> pspace_no_overlap' w1 pageBits sa) \<and> is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> koTypeOf (KOArch (KOASIDPool makeObject)) = ArchT ASIDPoolT \<and> is_aligned w1 (objBitsKO (KOArch (KOASIDPool makeObject))) \<and> pspace_aligned' sa \<and> pspace_no_overlap' w1 (objBitsKO (KOArch (KOASIDPool makeObject))) sa\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 y. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2 y\<rbrace> getSlotCap w3 \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y\<rbrace>
 3. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2\<rbrace>
 4. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q41 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (4 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2 pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; is_aligned w1 pageBits \<and> valid_untyped' False w1 pageBits idx s \<and> w1 \<noteq> 0 \<and> minUntypedSizeBits \<le> pageBits \<and> pageBits \<le> maxUntypedSizeBits \<and> idx \<le> 2 ^ pageBits \<and> is_aligned (word_of_nat idx) minUntypedSizeBits\<rbrakk> \<Longrightarrow> \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 () pcap\<rbrace> updateFreeIndex w3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>ya s. w4 && mask local.asid_low_bits = 0 \<longrightarrow> invs' s \<and> ct_active' s \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) w2 s \<and> is_aligned w1 (Suc (Suc local.asid_low_bits)) \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> cte_wp_at' (\<lambda>a. cteCap a = capability.UntypedCap False w1 pageBits (2 ^ pageBits)) w3 s \<and> descendants_of' w3 (null_filter' (ctes_of s)) = {} \<and> valid_pspace' s \<and> caps_no_overlap'' w1 pageBits s \<and> caps_overlap_reserved' {w1..w1 + 2 ^ pageBits - 1} s \<and> cte_wp_at' (\<lambda>a. True) w3 s \<and> pspace_distinct' s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) w2 s \<and> is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> pspace_aligned' s \<and> pspace_no_overlap' w1 pageBits s\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 y. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2 y\<rbrace> getSlotCap w3 \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y\<rbrace>
 3. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2\<rbrace>
 4. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q41 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (4 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2 pcap. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; is_aligned w1 pageBits; minUntypedSizeBits \<le> pageBits; pageBits \<le> maxUntypedSizeBits; is_aligned (word_of_nat idx) minUntypedSizeBits; w1 \<noteq> 0; valid_untyped' False w1 pageBits idx s; idx \<le> 2 ^ pageBits\<rbrakk> \<Longrightarrow> \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 () pcap\<rbrace> updateFreeIndex w3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>r sa. w4 && mask local.asid_low_bits = 0 \<longrightarrow> invs' sa \<and> pspace_no_overlap' w1 pageBits sa \<and> caps_no_overlap'' w1 pageBits sa \<and> is_aligned w1 (Suc (Suc local.asid_low_bits)) \<and> is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> cte_wp_at' (\<lambda>a. True) w3 sa \<and> ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> descendants_of' w3 (ctes_of sa) = {} \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) w2 sa \<and> ct_active' sa \<and> caps_overlap_reserved' {w1..w1 + 2 ^ pageBits - 1} sa \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> cte_wp_at' (\<lambda>a. cteCap a = capability.UntypedCap False w1 pageBits (2 ^ pageBits)) w3 sa\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 y. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2 y\<rbrace> getSlotCap w3 \<lbrace>?B46 s w1 w2 w3 w4 cte idx x2 y\<rbrace>
 3. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q41 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>?B45 s w1 w2 w3 w4 cte idx x2\<rbrace>
 4. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q41 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (2 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'280 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>\<lambda>rv s. \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) w3 s \<and> (invs' s \<and> cte_wp_at' ((\<lambda>capa. isUntypedCap capa \<and> capFreeIndex capa \<le> max_free_index (capBlockSize cap) \<and> max_free_index (capBlockSize cap) \<le> 2 ^ capBlockSize capa \<and> is_aligned (word_of_nat (max_free_index (capBlockSize cap))) minUntypedSizeBits) \<circ> cteCap) w3 s) \<and> (pspace_no_overlap' w1 pageBits s \<and> valid_pspace' s \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) w3 s) \<and> (caps_no_overlap'' w1 pageBits s \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) w3 s) \<and> (cte_wp_at' (\<lambda>_. True) w3 s \<and> is_aligned w1 (Suc (Suc local.asid_low_bits))) \<and> (cte_wp_at' (\<lambda>_. True) w3 s \<and> is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4))) \<and> (cte_wp_at' (\<lambda>_. True) w3 s \<and> cte_wp_at' (if w3 = w3 then (\<lambda>a. True) \<circ> cteCap_update (capFreeIndex_update (K (max_free_index (capBlockSize cap)))) else (\<lambda>a. True)) w3 s) \<and> (cte_wp_at' (isUntypedCap \<circ> cteCap) w3 s \<and> ex_cte_cap_wp_to' (\<lambda>a. True) w2 s) \<and> (cte_wp_at' (\<lambda>_. True) w3 s \<and> Suc (Suc local.asid_low_bits) < word_bits) \<and> (cte_wp_at' (isUntypedCap \<circ> cteCap) w3 s \<and> descendants_of' w3 (ctes_of s) = {}) \<and> (cte_wp_at' (\<lambda>_. True) w3 s \<and> cte_wp_at' (if w3 = w2 then (\<lambda>a. cteCap a = capability.NullCap) \<circ> cteCap_update (capFreeIndex_update (K (max_free_index (capBlockSize cap)))) else (\<lambda>a. cteCap a = capability.NullCap)) w2 s) \<and> ct_active' s \<and> (valid_pspace' s \<and> descendants_range_in' {w1..w1 + 2 ^ pageBits - 1} w3 (ctes_of s) \<and> cte_wp_at' ((\<lambda>capa. {w1..w1 + 2 ^ pageBits - 1} \<subseteq> untypedRange capa \<and> usableUntypedRange (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) capa) \<inter> {w1..w1 + 2 ^ pageBits - 1} = {} \<and> isUntypedCap capa) \<circ> cteCap) w3 s) \<and> cte_wp_at' (\<lambda>_. True) w3 s \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> cte_wp_at' (if w3 = w3 then (\<lambda>a. cteCap a = capability.UntypedCap False w1 pageBits (2 ^ pageBits)) \<circ> cteCap_update (capFreeIndex_update (K (max_free_index (capBlockSize cap)))) else (\<lambda>a. cteCap a = capability.UntypedCap False w1 pageBits (2 ^ pageBits))) w3 s\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> ?P'280 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (2 subgoals):
 1. \<And>s w1 w2 w3 w4 cte idx x2. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; w4 && mask local.asid_low_bits = 0; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'280 s w1 w2 w3 w4 cte idx x2\<rbrace> deleteObjects w1 pageBits \<lbrace>\<lambda>r sa. invs' sa \<and> pspace_no_overlap' w1 pageBits sa \<and> caps_no_overlap'' w1 pageBits sa \<and> is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4)) \<and> cte_wp_at' (\<lambda>_. True) w3 sa \<and> ex_cte_cap_wp_to' (\<lambda>a. True) w2 sa \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> descendants_of' w3 (ctes_of sa) = {} \<and> cte_wp_at' (\<lambda>a. isUntypedCap (cteCap a)) w3 sa \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> (\<exists>x. cte_wp_at' (\<lambda>c. cteCap c = x) w3 sa \<and> cte_wp_at' (\<lambda>a. cteCap a = capability.NullCap) w2 sa \<and> ct_active' sa \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> cte_wp_at' (\<lambda>a. capFreeIndex_update (\<lambda>y. max_free_index (capBlockSize x)) (cteCap a) = capability.UntypedCap False w1 pageBits (2 ^ pageBits)) w3 sa \<and> cte_wp_at' (\<lambda>a. isUntypedCap (cteCap a) \<and> capFreeIndex (cteCap a) \<le> max_free_index (capBlockSize x) \<and> word_of_nat (max_free_index (capBlockSize x)) && mask minUntypedSizeBits = 0 \<and> max_free_index (capBlockSize x) \<le> 2 ^ capBlockSize (cteCap a)) w3 sa \<and> cte_wp_at' (\<lambda>a. isUntypedCap (cteCap a) \<and> {w1..w1 + 2 ^ pageBits - 1} \<subseteq> untypedRange (cteCap a) \<and> usableUntypedRange (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize x)) (cteCap a)) \<inter> {w1..w1 + 2 ^ pageBits - 1} = {}) w3 sa)\<rbrace>
 2. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> ?P'280 s w1 w2 w3 w4 cte idx x2 sa proof (prove)
goal (1 subgoal):
 1. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d327 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx327 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d327 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx327 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) (ctes_of sa)) and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (valid_cap' (capability.UntypedCap (?d329 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx329 s w1 w2 w3 w4 cte idx x2)) and valid_pspace') sa \<and> (invs' sa \<and> ct_active' sa \<and> sch_act_simple sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d331 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx331 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) sa \<and> caps_no_overlap'' w1 pageBits sa \<and> descendants_range' (capability.UntypedCap (?d331 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx331 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) (ctes_of sa)) \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d333 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx333 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d333 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx333 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) (ctes_of sa)) and (\<lambda>s. is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4))) and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>_. True) w3 sa \<and> w3 \<notin> {w1..w1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d335 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx335 s w1 w2 w3 w4 cte idx x2)) sa \<and> valid_pspace' sa) \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d337 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx337 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d337 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx337 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) (ctes_of sa)) and ex_cte_cap_wp_to' (\<lambda>_. True) w2 and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d339 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx339 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d339 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx339 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) (ctes_of sa)) and (\<lambda>s. Suc (Suc local.asid_low_bits) < word_bits) and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d341 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx341 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d341 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx341 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) (ctes_of sa)) and (\<lambda>s. descendants_of' w3 (ctes_of s) = {}) and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>a. isUntypedCap (cteCap a)) w3 sa \<and> w3 \<notin> {w1..w1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d343 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx343 s w1 w2 w3 w4 cte idx x2)) sa \<and> valid_pspace' sa) \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d345 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx345 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d345 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx345 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) (ctes_of sa)) and (\<lambda>s. w1 && mask (Suc (Suc local.asid_low_bits)) = 0) and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (\<exists>x. (cte_wp_at' (\<lambda>c. cteCap c = x) w3 sa \<and> w3 \<notin> {w1..w1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d348 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx348 s w1 w2 w3 w4 cte idx x2 x)) sa \<and> valid_pspace' sa) \<and> (cte_wp_at' (\<lambda>a. cteCap a = capability.NullCap) w2 sa \<and> w2 \<notin> {w1..w1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d350 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx350 s w1 w2 w3 w4 cte idx x2 x)) sa \<and> valid_pspace' sa) \<and> (invs' and sch_act_simple and ct_active' and cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d352 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx352 s w1 w2 w3 w4 cte idx x2 x)) (makePoolParent aci) and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d352 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx352 s w1 w2 w3 w4 cte idx x2 x)) (makePoolParent aci) (ctes_of sa)) and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d354 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx354 s w1 w2 w3 w4 cte idx x2 x)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d354 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx354 s w1 w2 w3 w4 cte idx x2 x)) (makePoolParent aci) (ctes_of sa)) and (\<lambda>s. {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {}) and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>a. capFreeIndex_update (\<lambda>y. max_free_index (capBlockSize x)) (cteCap a) = capability.UntypedCap False w1 pageBits (2 ^ pageBits)) w3 sa \<and> w3 \<notin> {w1..w1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d356 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx356 s w1 w2 w3 w4 cte idx x2 x)) sa \<and> valid_pspace' sa) \<and> (cte_wp_at' (\<lambda>a. isUntypedCap (cteCap a) \<and> capFreeIndex (cteCap a) \<le> max_free_index (capBlockSize x) \<and> word_of_nat (max_free_index (capBlockSize x)) && mask minUntypedSizeBits = 0 \<and> max_free_index (capBlockSize x) \<le> 2 ^ capBlockSize (cteCap a)) w3 sa \<and> w3 \<notin> {w1..w1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d358 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx358 s w1 w2 w3 w4 cte idx x2 x)) sa \<and> valid_pspace' sa) \<and> cte_wp_at' (\<lambda>a. isUntypedCap (cteCap a) \<and> {w1..w1 + 2 ^ pageBits - 1} \<subseteq> untypedRange (cteCap a) \<and> usableUntypedRange (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize x)) (cteCap a)) \<inter> {w1..w1 + 2 ^ pageBits - 1} = {}) w3 sa \<and> w3 \<notin> {w1..w1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d359 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx359 s w1 w2 w3 w4 cte idx x2 x)) sa \<and> valid_pspace' sa) proof (prove)
goal (1 subgoal):
 1. \<And>s w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' s; ct_active' s; ctes_of s w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of s) = {}; ctes_of s w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 s; sch_act_simple s; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) s; s = sa; capAligned (capability.UntypedCap False w1 pageBits idx)\<rbrakk> \<Longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d327 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx327 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d327 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx327 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) (ctes_of sa)) and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (valid_cap' (capability.UntypedCap (?d329 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx329 s w1 w2 w3 w4 cte idx x2)) and valid_pspace') sa \<and> (invs' sa \<and> ct_active' sa \<and> sch_act_simple sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d331 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx331 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) sa \<and> caps_no_overlap'' w1 pageBits sa \<and> descendants_range' (capability.UntypedCap (?d331 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx331 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) (ctes_of sa)) \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d333 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx333 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d333 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx333 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) (ctes_of sa)) and (\<lambda>s. is_simple_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap w1 w4))) and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>_. True) w3 sa \<and> w3 \<notin> {w1..w1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d335 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx335 s w1 w2 w3 w4 cte idx x2)) sa \<and> valid_pspace' sa) \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d337 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx337 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d337 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx337 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) (ctes_of sa)) and ex_cte_cap_wp_to' (\<lambda>_. True) w2 and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d339 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx339 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d339 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx339 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) (ctes_of sa)) and (\<lambda>s. Suc (Suc local.asid_low_bits) < word_bits) and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d341 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx341 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d341 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx341 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) (ctes_of sa)) and (\<lambda>s. descendants_of' w3 (ctes_of s) = {}) and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>a. isUntypedCap (cteCap a)) w3 sa \<and> w3 \<notin> {w1..w1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d343 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx343 s w1 w2 w3 w4 cte idx x2)) sa \<and> valid_pspace' sa) \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d345 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx345 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d345 s w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx345 s w1 w2 w3 w4 cte idx x2)) (makePoolParent aci) (ctes_of sa)) and (\<lambda>s. w1 && mask (Suc (Suc local.asid_low_bits)) = 0) and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (\<exists>x. (cte_wp_at' (\<lambda>c. cteCap c = x) w3 sa \<and> w3 \<notin> {w1..w1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d348 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx348 s w1 w2 w3 w4 cte idx x2 x)) sa \<and> valid_pspace' sa) \<and> (cte_wp_at' (\<lambda>a. cteCap a = capability.NullCap) w2 sa \<and> w2 \<notin> {w1..w1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d350 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx350 s w1 w2 w3 w4 cte idx x2 x)) sa \<and> valid_pspace' sa) \<and> (invs' and sch_act_simple and ct_active' and cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d352 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx352 s w1 w2 w3 w4 cte idx x2 x)) (makePoolParent aci) and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d352 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx352 s w1 w2 w3 w4 cte idx x2 x)) (makePoolParent aci) (ctes_of sa)) and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d354 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx354 s w1 w2 w3 w4 cte idx x2 x)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d354 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx354 s w1 w2 w3 w4 cte idx x2 x)) (makePoolParent aci) (ctes_of sa)) and (\<lambda>s. {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {}) and K (pageBits < word_bits \<and> is_aligned w1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>a. capFreeIndex_update (\<lambda>y. max_free_index (capBlockSize x)) (cteCap a) = capability.UntypedCap False w1 pageBits (2 ^ pageBits)) w3 sa \<and> w3 \<notin> {w1..w1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d356 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx356 s w1 w2 w3 w4 cte idx x2 x)) sa \<and> valid_pspace' sa) \<and> (cte_wp_at' (\<lambda>a. isUntypedCap (cteCap a) \<and> capFreeIndex (cteCap a) \<le> max_free_index (capBlockSize x) \<and> word_of_nat (max_free_index (capBlockSize x)) && mask minUntypedSizeBits = 0 \<and> max_free_index (capBlockSize x) \<le> 2 ^ capBlockSize (cteCap a)) w3 sa \<and> w3 \<notin> {w1..w1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d358 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx358 s w1 w2 w3 w4 cte idx x2 x)) sa \<and> valid_pspace' sa) \<and> cte_wp_at' (\<lambda>a. isUntypedCap (cteCap a) \<and> {w1..w1 + 2 ^ pageBits - 1} \<subseteq> untypedRange (cteCap a) \<and> usableUntypedRange (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize x)) (cteCap a)) \<inter> {w1..w1 + 2 ^ pageBits - 1} = {}) w3 sa \<and> w3 \<notin> {w1..w1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d359 s w1 w2 w3 w4 cte idx x2 x) w1 pageBits (?idx359 s w1 w2 w3 w4 cte idx x2 x)) sa \<and> valid_pspace' sa) proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> \<not> ?d327 sa w1 w2 w3 w4 cte idx x2 \<and> idx = ?idx327 sa w1 w2 w3 w4 cte idx x2 \<and> descendants_range' (capability.UntypedCap (?d327 sa w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx327 sa w1 w2 w3 w4 cte idx x2)) w3 (ctes_of sa) \<and> valid_cap' (capability.UntypedCap (?d329 sa w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx329 sa w1 w2 w3 w4 cte idx x2)) sa \<and> \<not> ?d331 sa w1 w2 w3 w4 cte idx x2 \<and> idx = ?idx331 sa w1 w2 w3 w4 cte idx x2 \<and> caps_no_overlap'' w1 pageBits sa \<and> descendants_range' (capability.UntypedCap (?d331 sa w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx331 sa w1 w2 w3 w4 cte idx x2)) w3 (ctes_of sa) \<and> \<not> ?d333 sa w1 w2 w3 w4 cte idx x2 \<and> idx = ?idx333 sa w1 w2 w3 w4 cte idx x2 \<and> descendants_range' (capability.UntypedCap (?d333 sa w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx333 sa w1 w2 w3 w4 cte idx x2)) w3 (ctes_of sa) \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> valid_cap' (capability.UntypedCap (?d335 sa w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx335 sa w1 w2 w3 w4 cte idx x2)) sa \<and> \<not> ?d337 sa w1 w2 w3 w4 cte idx x2 \<and> idx = ?idx337 sa w1 w2 w3 w4 cte idx x2 \<and> descendants_range' (capability.UntypedCap (?d337 sa w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx337 sa w1 w2 w3 w4 cte idx x2)) w3 (ctes_of sa) \<and> \<not> ?d339 sa w1 w2 w3 w4 cte idx x2 \<and> idx = ?idx339 sa w1 w2 w3 w4 cte idx x2 \<and> descendants_range' (capability.UntypedCap (?d339 sa w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx339 sa w1 w2 w3 w4 cte idx x2)) w3 (ctes_of sa) \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> \<not> ?d341 sa w1 w2 w3 w4 cte idx x2 \<and> idx = ?idx341 sa w1 w2 w3 w4 cte idx x2 \<and> descendants_range' (capability.UntypedCap (?d341 sa w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx341 sa w1 w2 w3 w4 cte idx x2)) w3 (ctes_of sa) \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> valid_cap' (capability.UntypedCap (?d343 sa w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx343 sa w1 w2 w3 w4 cte idx x2)) sa \<and> \<not> ?d345 sa w1 w2 w3 w4 cte idx x2 \<and> idx = ?idx345 sa w1 w2 w3 w4 cte idx x2 \<and> descendants_range' (capability.UntypedCap (?d345 sa w1 w2 w3 w4 cte idx x2) w1 pageBits (?idx345 sa w1 w2 w3 w4 cte idx x2)) w3 (ctes_of sa) \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> valid_cap' (capability.UntypedCap (?d348 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx)) w1 pageBits (?idx348 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx))) sa \<and> (w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1) \<and> valid_cap' (capability.UntypedCap (?d350 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx)) w1 pageBits (?idx350 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx))) sa \<and> \<not> ?d352 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx) \<and> idx = ?idx352 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx) \<and> descendants_range' (capability.UntypedCap (?d352 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx)) w1 pageBits (?idx352 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx))) w3 (ctes_of sa) \<and> \<not> ?d354 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx) \<and> idx = ?idx354 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx) \<and> descendants_range' (capability.UntypedCap (?d354 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx)) w1 pageBits (?idx354 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx))) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> max_free_index pageBits = 2 ^ pageBits \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> valid_cap' (capability.UntypedCap (?d356 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx)) w1 pageBits (?idx356 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx))) sa \<and> idx \<le> max_free_index pageBits \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> max_free_index pageBits = 2 ^ pageBits \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> valid_cap' (capability.UntypedCap (?d358 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx)) w1 pageBits (?idx358 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx))) sa \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> valid_cap' (capability.UntypedCap (?d359 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx)) w1 pageBits (?idx359 sa w1 w2 w3 w4 cte idx x2 (capability.UntypedCap False w1 pageBits idx))) sa) proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> \<not> \<not> True \<and> True \<and> descendants_range' (capability.UntypedCap (?t380 w1 w2 w3 w4 cte idx x2 sa \<noteq> ?t380 w1 w2 w3 w4 cte idx x2 sa) w1 pageBits idx) w3 (ctes_of sa) \<and> valid_objs' sa \<and> \<not> \<not> True \<and> True \<and> caps_no_overlap'' w1 pageBits sa \<and> descendants_range' (capability.UntypedCap (?t396 w1 w2 w3 w4 cte idx x2 sa \<noteq> ?t396 w1 w2 w3 w4 cte idx x2 sa) w1 pageBits idx) w3 (ctes_of sa) \<and> \<not> \<not> True \<and> True \<and> descendants_range' (capability.UntypedCap (?t409 w1 w2 w3 w4 cte idx x2 sa \<noteq> ?t409 w1 w2 w3 w4 cte idx x2 sa) w1 pageBits idx) w3 (ctes_of sa) \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> valid_objs' sa \<and> \<not> \<not> True \<and> True \<and> descendants_range' (capability.UntypedCap (?t426 w1 w2 w3 w4 cte idx x2 sa \<noteq> ?t426 w1 w2 w3 w4 cte idx x2 sa) w1 pageBits idx) w3 (ctes_of sa) \<and> \<not> \<not> True \<and> True \<and> descendants_range' (capability.UntypedCap (?t438 w1 w2 w3 w4 cte idx x2 sa \<noteq> ?t438 w1 w2 w3 w4 cte idx x2 sa) w1 pageBits idx) w3 (ctes_of sa) \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> \<not> \<not> True \<and> True \<and> descendants_range' (capability.UntypedCap (?t451 w1 w2 w3 w4 cte idx x2 sa \<noteq> ?t451 w1 w2 w3 w4 cte idx x2 sa) w1 pageBits idx) w3 (ctes_of sa) \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> valid_objs' sa \<and> \<not> \<not> True \<and> True \<and> descendants_range' (capability.UntypedCap (?t468 w1 w2 w3 w4 cte idx x2 sa \<noteq> ?t468 w1 w2 w3 w4 cte idx x2 sa) w1 pageBits idx) w3 (ctes_of sa) \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> valid_objs' sa \<and> (w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1) \<and> valid_objs' sa \<and> \<not> \<not> True \<and> True \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> \<not> \<not> True \<and> True \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> max_free_index pageBits = 2 ^ pageBits \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> valid_objs' sa \<and> idx \<le> max_free_index pageBits \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> max_free_index pageBits = 2 ^ pageBits \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> valid_objs' sa \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> valid_objs' sa)
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> caps_no_overlap'' w1 pageBits sa \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> (w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1) \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (3 subgoals):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d560 w1 w2 w3 w4 cte idx x2 sa) (w1 && ~~ mask pageBits) pageBits (?idx560 w1 w2 w3 w4 cte idx x2 sa)) (?cref560 w1 w2 w3 w4 cte idx x2 sa) sa
 2. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits\<rbrakk> \<Longrightarrow> descendants_range_in' {w1..(w1 && ~~ mask pageBits) + 2 ^ pageBits - 1} (?cref560 w1 w2 w3 w4 cte idx x2 sa) (ctes_of sa)
 3. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> caps_no_overlap'' w1 pageBits sa \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> (w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1) \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (2 subgoals):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits\<rbrakk> \<Longrightarrow> descendants_range_in' {w1..(w1 && ~~ mask pageBits) + 2 ^ pageBits - 1} w3 (ctes_of sa)
 2. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> caps_no_overlap'' w1 pageBits sa \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> (w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1) \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> caps_no_overlap'' w1 pageBits sa \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> (w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1) \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (2 subgoals):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea \<noteq> capability.NullCap) (?p569 w1 w2 w3 w4 cte idx x2 sa) sa
 2. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; ex_cte_cap_wp_to' (\<lambda>_. True) (?p569 w1 w2 w3 w4 cte idx x2 sa) sa\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> caps_no_overlap'' w1 pageBits sa \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> (w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1) \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; ex_cte_cap_wp_to' (\<lambda>_. True) w2 sa; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; ex_cte_cap_wp_to' (\<lambda>_. True) w3 sa\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> caps_no_overlap'' w1 pageBits sa \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> (w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1) \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (5 subgoals):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; ex_cte_cap_wp_to' (\<lambda>_. True) w3 sa\<rbrakk> \<Longrightarrow> valid_global_refs' sa
 2. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; ex_cte_cap_wp_to' (\<lambda>_. True) w3 sa\<rbrakk> \<Longrightarrow> ctes_of sa (?cref579 w1 w2 w3 w4 cte idx x2 sa) = Some (CTE (capability.UntypedCap (?d579 w1 w2 w3 w4 cte idx x2 sa) (?ptr579 w1 w2 w3 w4 cte idx x2 sa) (?bits579 w1 w2 w3 w4 cte idx x2 sa) (?idx579 w1 w2 w3 w4 cte idx x2 sa)) (?mnode579 w1 w2 w3 w4 cte idx x2 sa))
 3. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; ex_cte_cap_wp_to' (\<lambda>_. True) w3 sa\<rbrakk> \<Longrightarrow> descendants_of' (?cref579 w1 w2 w3 w4 cte idx x2 sa) (ctes_of sa) = {}
 4. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; ex_cte_cap_wp_to' (\<lambda>_. True) w3 sa\<rbrakk> \<Longrightarrow> invs' sa
 5. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; ex_cte_cap_wp_to' (\<lambda>_. True) w3 sa; w2 \<notin> {?ptr579 w1 w2 w3 w4 cte idx x2 sa..?ptr579 w1 w2 w3 w4 cte idx x2 sa + 2 ^ ?bits579 w1 w2 w3 w4 cte idx x2 sa - 1}\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> caps_no_overlap'' w1 pageBits sa \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> (w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1) \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; ex_cte_cap_wp_to' (\<lambda>_. True) w3 sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (5 subgoals):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> valid_global_refs' sa
 2. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> ctes_of sa (?cref585 w1 w2 w3 w4 cte idx x2 sa) = Some (CTE (capability.UntypedCap (?d585 w1 w2 w3 w4 cte idx x2 sa) (?ptr585 w1 w2 w3 w4 cte idx x2 sa) (?bits585 w1 w2 w3 w4 cte idx x2 sa) (?idx585 w1 w2 w3 w4 cte idx x2 sa)) (?mnode585 w1 w2 w3 w4 cte idx x2 sa))
 3. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> descendants_of' (?cref585 w1 w2 w3 w4 cte idx x2 sa) (ctes_of sa) = {}
 4. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> invs' sa
 5. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1; w3 \<notin> {?ptr585 w1 w2 w3 w4 cte idx x2 sa..?ptr585 w1 w2 w3 w4 cte idx x2 sa + 2 ^ ?bits585 w1 w2 w3 w4 cte idx x2 sa - 1}\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> (w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1) \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1; w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (2 subgoals):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1; w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1; is_aligned (2 ^ pageBits) minUntypedSizeBits\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
 2. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1; w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> is_aligned (2 ^ pageBits) minUntypedSizeBits
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (2 subgoals):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1; w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> is_aligned (2 ^ pageBits) minUntypedSizeBits
 2. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1; w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1; is_aligned (2 ^ pageBits) minUntypedSizeBits\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (3 subgoals):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1; w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> is_aligned (2 ^ pageBits) (?x1100 w1 w2 w3 w4 cte idx x2 sa)
 2. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1; w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> minUntypedSizeBits \<le> ?x1100 w1 w2 w3 w4 cte idx x2 sa
 3. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1; w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1; is_aligned (2 ^ pageBits) minUntypedSizeBits\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (2 subgoals):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1; w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> minUntypedSizeBits \<le> pageBits
 2. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1; w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1; is_aligned (2 ^ pageBits) minUntypedSizeBits\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1; w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1; is_aligned (2 ^ pageBits) minUntypedSizeBits\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1; w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1; is_aligned (2 ^ pageBits) minUntypedSizeBits; kernel_data_refs \<inter> capRange (cteCap (CTE (capability.UntypedCap False w1 pageBits idx) x2)) = {} \<and> global_refs' sa \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> {w1..w1 + 2 ^ pageBits - 1} \<inter> kernel_data_refs = {} \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2 w3 w4 cte idx x2 sa. \<lbrakk>aci = asidcontrol_invocation.MakePool w1 w2 w3 w4; invs' sa; ct_active' sa; ctes_of sa w2 = Some cte; cteCap cte = capability.NullCap; descendants_of' w3 (ctes_of sa) = {}; ctes_of sa w3 = Some (CTE (capability.UntypedCap False w1 pageBits idx) x2); w2 \<noteq> w3; sch_act_simple sa; is_aligned w4 local.asid_low_bits; w4 < 2 ^ local.asid_bits; valid_cap' (capability.UntypedCap False w1 pageBits idx) sa; is_aligned w1 pageBits; caps_no_overlap'' w1 pageBits sa; w1 \<le> w2 \<longrightarrow> \<not> w2 \<le> w1 + 2 ^ pageBits - 1; w1 \<le> w3 \<longrightarrow> \<not> w3 \<le> w1 + 2 ^ pageBits - 1; is_aligned (2 ^ pageBits) minUntypedSizeBits; kernel_data_refs \<inter> {w1..w1 + 2 ^ pageBits - 1} = {} \<and> global_refs' sa \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> (max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits \<noteq> 0) \<and> (\<not> max_free_index pageBits < 2 ^ pageBits \<longrightarrow> w4 && mask local.asid_low_bits = 0 \<longrightarrow> idx \<le> max_free_index pageBits \<and> Suc (Suc local.asid_low_bits) < word_bits \<and> max_free_index pageBits = 2 ^ pageBits \<and> w1 && mask (Suc (Suc local.asid_low_bits)) = 0 \<and> word_of_nat (max_free_index pageBits) && mask minUntypedSizeBits = 0 \<and> descendants_range' (capability.UntypedCap False w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa) \<and> descendants_range' (capability.UntypedCap (?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<noteq> ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)) w1 pageBits idx) w3 (ctes_of sa))
flex-flex pairs:
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t509 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t508 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)
\<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t494 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx) \<equiv>\<^sup>? \<lambda>w1 w2 w3 w4 cte idx x2 sa. ?t493 w1 w2 w3 w4 cte idx x2 sa (capability.UntypedCap False w1 pageBits idx)