theory Arch_R

lemma performASIDControlInvocation_tcb_at':
  "\<lbrace>st_tcb_at' active' p and invs' and ct_active' and valid_aci' aci\<rbrace>
  performASIDControlInvocation aci
  \<lbrace>\<lambda>y. tcb_at' p\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: performASIDControlInvocation_def split: asidcontrol_invocation.splits) apply (clarsimp simp: valid_aci'_def cte_wp_at_ctes_of cong: conj_cong) apply (wp hoare_weak_lift_imp  |simp add:placeNewObject_def2)+ apply (wp createObjects_orig_obj_at2' updateFreeIndex_pspace_no_overlap' getSlotCap_wp hoare_weak_lift_imp)+ apply (clarsimp simp: projectKO_opts_defs) apply (strengthen st_tcb_strg' [where P=\<top>]) apply (wp deleteObjects_invs_derivatives[where p="makePoolParent aci"]
     hoare_vcg_ex_lift deleteObjects_cte_wp_at'[where d=False]
     deleteObjects_st_tcb_at'[where p="makePoolParent aci"] hoare_weak_lift_imp
     updateFreeIndex_pspace_no_overlap' deleteObject_no_overlap[where d=False])+ apply (case_tac ctea) apply (clarsimp) apply (frule ctes_of_valid_cap') apply (simp add:invs_valid_objs')+ apply (clarsimp simp:valid_cap'_def capAligned_def cte_wp_at_ctes_of) apply (strengthen refl order_refl
                    pred_tcb'_weakenE[mk_strg I E]) apply (clarsimp simp: conj_comms invs_valid_pspace' isCap_simps
                        descendants_range'_def2 empty_descendants_range_in') apply (frule ctes_of_valid', clarsimp, simp,
    drule capFreeIndex_update_valid_cap'[where fb="2 ^ pageBits", rotated -1],
    simp_all) apply (simp add: pageBits_def is_aligned_def minUntypedSizeBits_def) apply (simp add: valid_cap_simps' range_cover_def objBits_simps archObjSize_def
                   capAligned_def unat_eq_0 and_mask_eq_iff_shiftr_0[symmetric]
                   word_bw_assocs untypedBits_defs) apply clarsimp apply (drule(1) cte_cap_in_untyped_range,
    fastforce simp add: cte_wp_at_ctes_of, assumption, simp_all) apply (clarsimp simp: invs'_def valid_state'_def if_unsafe_then_cap'_def cte_wp_at_ctes_of) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' active' p and invs' and ct_active' and valid_aci' aci\<rbrace> performASIDControlInvocation aci \<lbrace>\<lambda>y. tcb_at' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (st_tcb_at' active' p and invs' and ct_active' and valid_aci' aci) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> performASIDControlInvocation aci \<lbrace>\<lambda>y. tcb_at' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x3 x4. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; valid_aci' (asidcontrol_invocation.MakePool x1 x2 x3 x4) s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- deleteObjects x1 pageBits;
pcap <- getSlotCap x3;
y <- updateFreeIndex x3 (max_free_index (capBlockSize pcap));
y <- placeNewObject x1 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. tcb_at' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x3 x4 cte ctea idx. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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 <- placeNewObject x1 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. tcb_at' p\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s x1 x2 x3 x4 cte ctea idx pcap. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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>?P'45 s x1 x2 x3 x4 cte ctea idx () pcap ()\<rbrace> createObjects' x1 (Suc 0) (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>rv. tcb_at' p\<rbrace>
 2. \<And>s x1 x2 x3 x4 cte ctea idx y pcap. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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>?B30 s x1 x2 x3 x4 cte ctea idx y pcap\<rbrace> updateFreeIndex x3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>ya sa. x4 && mask local.asid_low_bits = 0 \<longrightarrow> ?P'45 s x1 x2 x3 x4 cte ctea idx y pcap ya sa\<rbrace>
 3. \<And>s x1 x2 x3 x4 cte ctea idx y. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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>?B29 s x1 x2 x3 x4 cte ctea idx y\<rbrace> getSlotCap x3 \<lbrace>?B30 s x1 x2 x3 x4 cte ctea idx y\<rbrace>
 4. \<And>s x1 x2 x3 x4 cte ctea idx. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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>?Q28 s x1 x2 x3 x4 cte ctea idx\<rbrace> deleteObjects x1 pageBits \<lbrace>?B29 s x1 x2 x3 x4 cte ctea idx\<rbrace>
 5. \<And>s x1 x2 x3 x4 cte ctea idx sa. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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; s = sa\<rbrakk> \<Longrightarrow> ?Q28 s x1 x2 x3 x4 cte ctea idx sa proof (prove)
goal (4 subgoals):
 1. \<And>s x1 x2 x3 x4 cte ctea idx y pcap. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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>?P'65 s x1 x2 x3 x4 cte ctea idx y pcap\<rbrace> updateFreeIndex x3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>rv sa. tcb_at' p sa \<and> \<not> (case projectKO_opt (KOArch (KOASIDPool makeObject)) of None \<Rightarrow> False | Some a \<Rightarrow> True) \<and> pspace_no_overlap' x1 (?sz51 s x1 x2 x3 x4 cte ctea idx y pcap rv) sa\<rbrace>
 2. \<And>s x1 x2 x3 x4 cte ctea idx y. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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>?B29 s x1 x2 x3 x4 cte ctea idx y\<rbrace> getSlotCap x3 \<lbrace>\<lambda>pcap sa. x4 && mask local.asid_low_bits = 0 \<longrightarrow> Suc 0 \<noteq> 0 \<and> range_cover x1 (?sz62 s x1 x2 x3 x4 cte ctea idx y pcap) (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ?P'65 s x1 x2 x3 x4 cte ctea idx y pcap sa\<rbrace>
 3. \<And>s x1 x2 x3 x4 cte ctea idx. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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>?Q28 s x1 x2 x3 x4 cte ctea idx\<rbrace> deleteObjects x1 pageBits \<lbrace>?B29 s x1 x2 x3 x4 cte ctea idx\<rbrace>
 4. \<And>s x1 x2 x3 x4 cte ctea idx sa. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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; s = sa\<rbrakk> \<Longrightarrow> ?Q28 s x1 x2 x3 x4 cte ctea idx sa
flex-flex pairs:
\<lambda>s x1 x2 x3 x4 cte ctea idx. ?sz62 s x1 x2 x3 x4 cte ctea idx () \<equiv>\<^sup>? \<lambda>s x1 x2 x3 x4 cte ctea idx pcap. ?sz51 s x1 x2 x3 x4 cte ctea idx () pcap () proof (prove)
goal (4 subgoals):
 1. \<And>s x1 x2 x3 x4 cte ctea idx pcap. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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>?P'65 s x1 x2 x3 x4 cte ctea idx () pcap\<rbrace> updateFreeIndex x3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>rv sa. tcb_at' p sa \<and> pspace_no_overlap' x1 (?sz51 s x1 x2 x3 x4 cte ctea idx () pcap ()) sa\<rbrace>
 2. \<And>s x1 x2 x3 x4 cte ctea idx y. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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>?B29 s x1 x2 x3 x4 cte ctea idx y\<rbrace> getSlotCap x3 \<lbrace>\<lambda>pcap sa. x4 && mask local.asid_low_bits = 0 \<longrightarrow> Suc 0 \<noteq> 0 \<and> range_cover x1 (?sz62 s x1 x2 x3 x4 cte ctea idx y pcap) (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ?P'65 s x1 x2 x3 x4 cte ctea idx y pcap sa\<rbrace>
 3. \<And>s x1 x2 x3 x4 cte ctea idx. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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>?Q28 s x1 x2 x3 x4 cte ctea idx\<rbrace> deleteObjects x1 pageBits \<lbrace>?B29 s x1 x2 x3 x4 cte ctea idx\<rbrace>
 4. \<And>s x1 x2 x3 x4 cte ctea idx sa. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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; s = sa\<rbrakk> \<Longrightarrow> ?Q28 s x1 x2 x3 x4 cte ctea idx sa
flex-flex pairs:
\<lambda>s x1 x2 x3 x4 cte ctea idx. ?sz62 s x1 x2 x3 x4 cte ctea idx () \<equiv>\<^sup>? \<lambda>s x1 x2 x3 x4 cte ctea idx pcap. ?sz51 s x1 x2 x3 x4 cte ctea idx () pcap () proof (prove)
goal (4 subgoals):
 1. \<And>s x1 x2 x3 x4 cte ctea idx pcap. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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>?P'65 s x1 x2 x3 x4 cte ctea idx () pcap\<rbrace> updateFreeIndex x3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>r sa. st_tcb_at' (\<lambda>_. True) p sa \<and> pspace_no_overlap' x1 (?sz51 s x1 x2 x3 x4 cte ctea idx () pcap ()) sa\<rbrace>
 2. \<And>s x1 x2 x3 x4 cte ctea idx y. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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>?B29 s x1 x2 x3 x4 cte ctea idx y\<rbrace> getSlotCap x3 \<lbrace>\<lambda>pcap sa. x4 && mask local.asid_low_bits = 0 \<longrightarrow> Suc 0 \<noteq> 0 \<and> range_cover x1 (?sz62 s x1 x2 x3 x4 cte ctea idx y pcap) (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> ?P'65 s x1 x2 x3 x4 cte ctea idx y pcap sa\<rbrace>
 3. \<And>s x1 x2 x3 x4 cte ctea idx. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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>?Q28 s x1 x2 x3 x4 cte ctea idx\<rbrace> deleteObjects x1 pageBits \<lbrace>?B29 s x1 x2 x3 x4 cte ctea idx\<rbrace>
 4. \<And>s x1 x2 x3 x4 cte ctea idx sa. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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; s = sa\<rbrakk> \<Longrightarrow> ?Q28 s x1 x2 x3 x4 cte ctea idx sa
flex-flex pairs:
\<lambda>s x1 x2 x3 x4 cte ctea idx. ?sz62 s x1 x2 x3 x4 cte ctea idx () \<equiv>\<^sup>? \<lambda>s x1 x2 x3 x4 cte ctea idx pcap. ?sz51 s x1 x2 x3 x4 cte ctea idx () pcap () proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x3 x4 cte ctea idx sa. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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; s = sa\<rbrakk> \<Longrightarrow> x4 && mask local.asid_low_bits = 0 \<longrightarrow> Suc 0 \<noteq> 0 \<and> range_cover x1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d108 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx108 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d108 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx108 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) (ctes_of sa)) and K (pageBits < word_bits \<and> is_aligned x1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d110 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx110 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d110 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx110 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) (ctes_of sa)) and K (pageBits < word_bits \<and> is_aligned x1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d112 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx112 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d112 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx112 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) (ctes_of sa)) and st_tcb_at' ((\<lambda>a. True) and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) p and K (pageBits < word_bits \<and> is_aligned x1 pageBits)) sa \<and> (valid_cap' (capability.UntypedCap False x1 pageBits (?idx114 s x1 x2 x3 x4 cte ctea idx)) and valid_pspace') sa \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d116 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx116 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d116 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx116 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) (ctes_of sa)) and K (pageBits < word_bits \<and> is_aligned x1 pageBits)) sa \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) x3 sa \<and> x3 \<notin> {x1..x1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap False x1 pageBits (?idx117 s x1 x2 x3 x4 cte ctea idx)) sa \<and> valid_pspace' sa proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x3 x4 cte ctea idx sa x1a x2a. \<lbrakk>st_tcb_at' active' p s; invs' s; ct_active' s; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; 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; s = sa; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> x4 && mask local.asid_low_bits = 0 \<longrightarrow> Suc 0 \<noteq> 0 \<and> range_cover x1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject)) + 0) (Suc 0) \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d108 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx108 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d108 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx108 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) (ctes_of sa)) and K (pageBits < word_bits \<and> is_aligned x1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d110 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx110 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d110 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx110 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) (ctes_of sa)) and K (pageBits < word_bits \<and> is_aligned x1 pageBits)) sa \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d112 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx112 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d112 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx112 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) (ctes_of sa)) and st_tcb_at' ((\<lambda>a. True) and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) p and K (pageBits < word_bits \<and> is_aligned x1 pageBits)) sa \<and> (valid_cap' (capability.UntypedCap False x1 pageBits (?idx114 s x1 x2 x3 x4 cte ctea idx)) and valid_pspace') sa \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d116 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx116 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d116 s x1 x2 x3 x4 cte ctea idx) x1 pageBits (?idx116 s x1 x2 x3 x4 cte ctea idx)) (makePoolParent aci) (ctes_of sa)) and K (pageBits < word_bits \<and> is_aligned x1 pageBits)) sa \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) x3 sa \<and> x3 \<notin> {x1..x1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap False x1 pageBits (?idx117 s x1 x2 x3 x4 cte ctea idx)) sa \<and> valid_pspace' sa proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> range_cover x1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject))) (Suc 0) \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 sa \<and> descendants_range' (capability.UntypedCap (?d108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> is_aligned x1 pageBits \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 sa \<and> descendants_range' (capability.UntypedCap (?d110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> is_aligned x1 pageBits \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 sa \<and> descendants_range' (capability.UntypedCap (?d112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> st_tcb_at' ((\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) p sa \<and> is_aligned x1 pageBits \<and> valid_cap' (capability.UntypedCap False x1 pageBits (?idx114 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) sa \<and> valid_pspace' sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 sa \<and> descendants_range' (capability.UntypedCap (?d116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> is_aligned x1 pageBits \<and> cte_wp_at' (\<lambda>a. isUntypedCap (cteCap a)) x3 sa \<and> (x1 \<le> x3 \<longrightarrow> \<not> x3 \<le> x1 + 2 ^ pageBits - 1) \<and> valid_cap' (capability.UntypedCap False x1 pageBits (?idx117 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) sa \<and> valid_pspace' sa proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> valid_objs' sa
 2. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0; valid_cap' (capability.UntypedCap False x1 pageBits idx) sa\<rbrakk> \<Longrightarrow> range_cover x1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject))) (Suc 0) \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 sa \<and> descendants_range' (capability.UntypedCap (?d108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> is_aligned x1 pageBits \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 sa \<and> descendants_range' (capability.UntypedCap (?d110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> is_aligned x1 pageBits \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 sa \<and> descendants_range' (capability.UntypedCap (?d112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> st_tcb_at' ((\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) p sa \<and> is_aligned x1 pageBits \<and> valid_cap' (capability.UntypedCap False x1 pageBits (?idx114 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) sa \<and> valid_pspace' sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 sa \<and> descendants_range' (capability.UntypedCap (?d116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> is_aligned x1 pageBits \<and> cte_wp_at' (\<lambda>a. isUntypedCap (cteCap a)) x3 sa \<and> (x1 \<le> x3 \<longrightarrow> \<not> x3 \<le> x1 + 2 ^ pageBits - 1) \<and> valid_cap' (capability.UntypedCap False x1 pageBits (?idx117 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) sa \<and> valid_pspace' sa proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0; valid_cap' (capability.UntypedCap False x1 pageBits idx) sa\<rbrakk> \<Longrightarrow> range_cover x1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject))) (Suc 0) \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 sa \<and> descendants_range' (capability.UntypedCap (?d108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> is_aligned x1 pageBits \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 sa \<and> descendants_range' (capability.UntypedCap (?d110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> is_aligned x1 pageBits \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 sa \<and> descendants_range' (capability.UntypedCap (?d112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> st_tcb_at' ((\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) p sa \<and> is_aligned x1 pageBits \<and> valid_cap' (capability.UntypedCap False x1 pageBits (?idx114 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) sa \<and> valid_pspace' sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 sa \<and> descendants_range' (capability.UntypedCap (?d116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> is_aligned x1 pageBits \<and> cte_wp_at' (\<lambda>a. isUntypedCap (cteCap a)) x3 sa \<and> (x1 \<le> x3 \<longrightarrow> \<not> x3 \<le> x1 + 2 ^ pageBits - 1) \<and> valid_cap' (capability.UntypedCap False x1 pageBits (?idx117 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) sa \<and> valid_pspace' sa proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0; is_aligned x1 pageBits; valid_untyped' False x1 pageBits idx sa; x1 \<noteq> 0; minUntypedSizeBits \<le> pageBits; pageBits \<le> maxUntypedSizeBits; idx \<le> 2 ^ pageBits; is_aligned (word_of_nat idx) minUntypedSizeBits\<rbrakk> \<Longrightarrow> range_cover x1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject))) (Suc 0) \<and> \<not> ?d108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<and> idx = ?idx108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<and> descendants_range' (capability.UntypedCap (?d108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx108 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> \<not> ?d110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<and> idx = ?idx110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<and> descendants_range' (capability.UntypedCap (?d110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx110 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> \<not> ?d112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<and> idx = ?idx112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<and> descendants_range' (capability.UntypedCap (?d112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx112 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> st_tcb_at' ((\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) p sa \<and> valid_untyped' False x1 pageBits (?idx114 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) sa \<and> ?idx114 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<le> 2 ^ pageBits \<and> is_aligned (word_of_nat (?idx114 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) minUntypedSizeBits \<and> valid_pspace' sa \<and> \<not> ?d116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<and> idx = ?idx116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<and> descendants_range' (capability.UntypedCap (?d116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits (?idx116 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) x3 (ctes_of sa) \<and> (x1 \<le> x3 \<longrightarrow> \<not> x3 \<le> x1 + 2 ^ pageBits - 1) \<and> valid_untyped' False x1 pageBits (?idx117 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) sa \<and> ?idx117 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<le> 2 ^ pageBits \<and> is_aligned (word_of_nat (?idx117 sa x1 x2 x3 x4 cte (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx)) minUntypedSizeBits \<and> valid_pspace' sa proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0; is_aligned x1 pageBits; valid_untyped' False x1 pageBits idx sa; x1 \<noteq> 0; minUntypedSizeBits \<le> pageBits; pageBits \<le> maxUntypedSizeBits; idx \<le> 2 ^ pageBits; is_aligned (word_of_nat idx) minUntypedSizeBits\<rbrakk> \<Longrightarrow> range_cover x1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject))) (Suc 0) \<and> \<not> \<not> True \<and> True \<and> descendants_range' (capability.UntypedCap (?t146 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<noteq> ?t145 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits idx) x3 (ctes_of sa) \<and> \<not> \<not> True \<and> True \<and> descendants_range' (capability.UntypedCap (?t161 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<noteq> ?t160 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits idx) x3 (ctes_of sa) \<and> \<not> \<not> True \<and> True \<and> descendants_range' (capability.UntypedCap (?t176 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<noteq> ?t175 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits idx) x3 (ctes_of sa) \<and> (\<forall>st. active' st \<longrightarrow> ((\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) st) \<and> valid_untyped' False x1 pageBits (2 ^ pageBits) sa \<and> True \<and> is_aligned (word_of_nat (2 ^ pageBits)) minUntypedSizeBits \<and> valid_pspace' sa \<and> \<not> \<not> True \<and> True \<and> descendants_range' (capability.UntypedCap (?t201 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<noteq> ?t200 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx) x1 pageBits idx) x3 (ctes_of sa) \<and> (x1 \<le> x3 \<longrightarrow> \<not> x3 \<le> x1 + 2 ^ pageBits - 1) \<and> valid_untyped' False x1 pageBits (2 ^ pageBits) sa \<and> True \<and> is_aligned (word_of_nat (2 ^ pageBits)) minUntypedSizeBits \<and> valid_pspace' sa
flex-flex pairs:
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t201 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t200 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t176 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t175 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t161 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t160 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t146 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t145 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0; is_aligned x1 pageBits; valid_untyped' False x1 pageBits idx sa; x1 \<noteq> 0; minUntypedSizeBits \<le> pageBits; pageBits \<le> maxUntypedSizeBits; idx \<le> 2 ^ pageBits; is_aligned (word_of_nat idx) minUntypedSizeBits\<rbrakk> \<Longrightarrow> is_aligned (2 ^ pageBits) minUntypedSizeBits \<and> range_cover x1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject))) (Suc 0) \<and> valid_untyped' False x1 pageBits (2 ^ pageBits) sa \<and> (x1 \<le> x3 \<longrightarrow> \<not> x3 \<le> x1 + 2 ^ pageBits - 1)
flex-flex pairs:
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t201 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t200 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t176 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t175 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t161 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t160 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t146 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t145 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0; is_aligned x1 pageBits; valid_untyped' False x1 pageBits idx sa; x1 \<noteq> 0; minUntypedSizeBits \<le> pageBits; pageBits \<le> maxUntypedSizeBits; idx \<le> 2 ^ pageBits; is_aligned (word_of_nat idx) minUntypedSizeBits\<rbrakk> \<Longrightarrow> is_aligned (2 ^ pageBits) minUntypedSizeBits
 2. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0; is_aligned x1 pageBits; valid_untyped' False x1 pageBits idx sa; x1 \<noteq> 0; minUntypedSizeBits \<le> pageBits; pageBits \<le> maxUntypedSizeBits; idx \<le> 2 ^ pageBits; is_aligned (word_of_nat idx) minUntypedSizeBits; valid_cap' (capability.UntypedCap False x1 pageBits (2 ^ pageBits)) sa\<rbrakk> \<Longrightarrow> is_aligned (2 ^ pageBits) minUntypedSizeBits \<and> range_cover x1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject))) (Suc 0) \<and> valid_untyped' False x1 pageBits (2 ^ pageBits) sa \<and> (x1 \<le> x3 \<longrightarrow> \<not> x3 \<le> x1 + 2 ^ pageBits - 1)
flex-flex pairs:
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t201 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t200 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t176 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t175 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t161 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t160 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t146 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t145 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0; is_aligned x1 pageBits; valid_untyped' False x1 pageBits idx sa; x1 \<noteq> 0; minUntypedSizeBits \<le> pageBits; pageBits \<le> maxUntypedSizeBits; idx \<le> 2 ^ pageBits; is_aligned (word_of_nat idx) minUntypedSizeBits; valid_cap' (capability.UntypedCap False x1 pageBits (2 ^ pageBits)) sa\<rbrakk> \<Longrightarrow> is_aligned (2 ^ pageBits) minUntypedSizeBits \<and> range_cover x1 pageBits (objBitsKO (KOArch (KOASIDPool makeObject))) (Suc 0) \<and> valid_untyped' False x1 pageBits (2 ^ pageBits) sa \<and> (x1 \<le> x3 \<longrightarrow> \<not> x3 \<le> x1 + 2 ^ pageBits - 1)
flex-flex pairs:
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t201 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t200 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t176 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t175 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t161 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t160 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t146 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t145 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0; is_aligned x1 pageBits; valid_untyped' False x1 pageBits idx sa; x1 \<noteq> 0; 4 \<le> pageBits; pageBits \<le> 29; idx \<le> 2 ^ pageBits; is_aligned (word_of_nat idx) 4; valid_untyped' False x1 pageBits (2 ^ pageBits) sa \<and> is_aligned (2 ^ pageBits) 4\<rbrakk> \<Longrightarrow> x1 \<le> x3 \<longrightarrow> \<not> x3 \<le> x1 + 2 ^ pageBits - 1
flex-flex pairs:
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t201 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t200 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t176 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t175 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t161 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t160 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t146 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t145 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0; is_aligned x1 pageBits; valid_untyped' False x1 pageBits idx sa; x1 \<noteq> 0; 4 \<le> pageBits; pageBits \<le> 29; idx \<le> 2 ^ pageBits; is_aligned (word_of_nat idx) 4; valid_untyped' False x1 pageBits (2 ^ pageBits) sa; is_aligned (2 ^ pageBits) 4; x1 \<le> x3; x3 \<le> x1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> False
flex-flex pairs:
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t201 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t200 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t176 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t175 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t161 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t160 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t146 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t145 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0; is_aligned x1 pageBits; valid_untyped' False x1 pageBits idx sa; x1 \<noteq> 0; 4 \<le> pageBits; pageBits \<le> 29; idx \<le> 2 ^ pageBits; is_aligned (word_of_nat idx) 4; valid_untyped' False x1 pageBits (2 ^ pageBits) sa; is_aligned (2 ^ pageBits) 4; x3 \<le> x1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) x3 sa
 2. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0; is_aligned x1 pageBits; valid_untyped' False x1 pageBits idx sa; x1 \<noteq> 0; 4 \<le> pageBits; pageBits \<le> 29; idx \<le> 2 ^ pageBits; is_aligned (word_of_nat idx) 4; valid_untyped' False x1 pageBits (2 ^ pageBits) sa; is_aligned (2 ^ pageBits) 4; x3 \<le> x1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> valid_global_refs' sa
flex-flex pairs:
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t201 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t200 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t176 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t175 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t161 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t160 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t146 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t145 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 cte idx sa x2a. \<lbrakk>st_tcb_at' active' p sa; invs' sa; ct_active' sa; aci = asidcontrol_invocation.MakePool x1 x2 x3 x4; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; x4 && mask local.asid_low_bits = 0; is_aligned x1 pageBits; valid_untyped' False x1 pageBits idx sa; x1 \<noteq> 0; 4 \<le> pageBits; pageBits \<le> 29; idx \<le> 2 ^ pageBits; is_aligned (word_of_nat idx) 4; valid_untyped' False x1 pageBits (2 ^ pageBits) sa; is_aligned (2 ^ pageBits) 4; x3 \<le> x1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> valid_global_refs' sa
flex-flex pairs:
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t201 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t200 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t176 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t175 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t161 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t160 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t146 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t145 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx proof (prove)
goal:
No subgoals!
flex-flex pairs:
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t201 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t200 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t176 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t175 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t161 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t160 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx
\<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t146 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx \<equiv>\<^sup>? \<lambda>x1 x2 x3 x4 cte idx sa x2a. ?t145 x1 x2 x3 x4 cte sa (CTE (capability.UntypedCap False x1 pageBits idx) x2a) idx