theory PageTableDuplicates

lemma invokeUntyped_valid_duplicates[wp]:
  notes whenE_wps[wp_split del] shows
  "\<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))
         and valid_untyped_inv' ui and ct_active'\<rbrace>
     invokeUntyped ui
   \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s) \<rbrace>" apply (simp only: invokeUntyped_def updateCap_def) apply (rule hoare_name_pre_state) apply (cases ui) apply (clarsimp simp only: pred_conj_def valid_untyped_inv_wcap'
                             Invocations_H.untyped_invocation.simps) apply (frule(2) invokeUntyped_proofs.intro) apply (rule hoare_pre) apply simp apply (wp add: updateFreeIndex_pspace_no_overlap') apply (rule hoare_post_impErr) apply (rule combine_validE) apply (rule_tac ui=ui in whenE_reset_resetUntypedCap_invs_etc) apply (rule whenE_wp) apply (rule valid_validE) apply (rule resetUntypedCap_valid_duplicates') defer apply simp apply (clarsimp simp del: valid_untyped_inv_wcap'.simps
                split del: if_split) apply (rule conjI, assumption) apply (auto simp: cte_wp_at_ctes_of isCap_simps)[1] apply (clarsimp simp: cte_wp_at_ctes_of) apply (frule new_CapTable_bound) apply (frule invokeUntyped_proofs.not_0_ptr) apply (strengthen is_aligned_armKSGlobalPD) apply (frule cte_wp_at_valid_objs_valid_cap'[OF ctes_of_cte_wpD], clarsimp+) apply (clarsimp simp add: isCap_simps valid_cap_simps' capAligned_def) apply (auto split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_untyped_inv' ui and ct_active'\<rbrace> invokeUntyped ui \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_untyped_inv' ui and ct_active'\<rbrace> case ui of Invocations_H.untyped_invocation.Retype srcSlot reset base retypeBase newType userSize destSlots isDev \<Rightarrow> doE whenE reset $ resetUntypedCap srcSlot;
withoutPreemption $ do totalObjectSize <- return (length destSlots `~shiftL~` getObjectSize newType userSize);
inRange <- return (\<lambda>x. fromPPtr retypeBase \<le> x \<and> x \<le> fromPPtr retypeBase + fromIntegral totalObjectSize - 1);
stateAssert (\<lambda>s. \<not> cNodeOverlap (gsCNodes s) inRange) [];
stateAssert (\<lambda>s. \<not> archOverlap s inRange) [];
haskell_assert (canonicalAddressAssert retypeBase) [];
freeRef <- return (retypeBase + PPtr (fromIntegral totalObjectSize));
updateFreeIndex srcSlot (getFreeIndex base freeRef);
createNewObjects newType srcSlot destSlots retypeBase userSize isDev
od
odE \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_untyped_inv' ui and ct_active') s \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ui of Invocations_H.untyped_invocation.Retype srcSlot reset base retypeBase newType userSize destSlots isDev \<Rightarrow> doE whenE reset $ resetUntypedCap srcSlot;
withoutPreemption $ do totalObjectSize <- return (length destSlots `~shiftL~` getObjectSize newType userSize);
inRange <- return (\<lambda>x. fromPPtr retypeBase \<le> x \<and> x \<le> fromPPtr retypeBase + fromIntegral totalObjectSize - 1);
stateAssert (\<lambda>s. \<not> cNodeOverlap (gsCNodes s) inRange) [];
stateAssert (\<lambda>s. \<not> archOverlap s inRange) [];
haskell_assert (canonicalAddressAssert retypeBase) [];
freeRef <- return (retypeBase + PPtr (fromIntegral totalObjectSize));
updateFreeIndex srcSlot (getFreeIndex base freeRef);
createNewObjects newType srcSlot destSlots retypeBase userSize isDev
od
odE \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8. \<lbrakk>(invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_untyped_inv' ui and ct_active') s; ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ui of Invocations_H.untyped_invocation.Retype srcSlot reset base retypeBase newType userSize destSlots isDev \<Rightarrow> doE whenE reset $ resetUntypedCap srcSlot;
withoutPreemption $ do totalObjectSize <- return (length destSlots `~shiftL~` getObjectSize newType userSize);
inRange <- return (\<lambda>x. fromPPtr retypeBase \<le> x \<and> x \<le> fromPPtr retypeBase + fromIntegral totalObjectSize - 1);
stateAssert (\<lambda>s. \<not> cNodeOverlap (gsCNodes s) inRange) [];
stateAssert (\<lambda>s. \<not> archOverlap s inRange) [];
haskell_assert (canonicalAddressAssert retypeBase) [];
freeRef <- return (retypeBase + PPtr (fromIntegral totalObjectSize));
updateFreeIndex srcSlot (getFreeIndex base freeRef);
createNewObjects newType srcSlot destSlots retypeBase userSize isDev
od
odE \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) s; invs' s; vs_valid_duplicates' (ksPSpace s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE whenE x2 $ resetUntypedCap x1;
withoutPreemption $ do totalObjectSize <- return (length x7 `~shiftL~` getObjectSize x5 x6);
inRange <- return (\<lambda>x. fromPPtr x4 \<le> x \<and> x \<le> fromPPtr x4 + fromIntegral totalObjectSize - 1);
stateAssert (\<lambda>s. \<not> cNodeOverlap (gsCNodes s) inRange) [];
stateAssert (\<lambda>s. \<not> archOverlap s inRange) [];
haskell_assert (canonicalAddressAssert x4) [];
freeRef <- return (x4 + PPtr (fromIntegral totalObjectSize));
updateFreeIndex x1 (getFreeIndex x3 freeRef);
createNewObjects x5 x1 x7 x4 x6 x8
od
odE \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE whenE x2 $ resetUntypedCap x1;
withoutPreemption $ do totalObjectSize <- return (length x7 `~shiftL~` getObjectSize x5 x6);
inRange <- return (\<lambda>x. fromPPtr x4 \<le> x \<and> x \<le> fromPPtr x4 + fromIntegral totalObjectSize - 1);
stateAssert (\<lambda>s. \<not> cNodeOverlap (gsCNodes s) inRange) [];
stateAssert (\<lambda>s. \<not> archOverlap s inRange) [];
haskell_assert (canonicalAddressAssert x4) [];
freeRef <- return (x4 + PPtr (fromIntegral totalObjectSize));
updateFreeIndex x1 (getFreeIndex x3 freeRef);
createNewObjects x5 x1 x7 x4 x6 x8
od
odE \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace> doE whenE x2 $ resetUntypedCap x1;
withoutPreemption $ do totalObjectSize <- return (length x7 `~shiftL~` getObjectSize x5 x6);
inRange <- return (\<lambda>x. fromPPtr x4 \<le> x \<and> x \<le> fromPPtr x4 + fromIntegral totalObjectSize - 1);
stateAssert (\<lambda>s. \<not> cNodeOverlap (gsCNodes s) inRange) [];
stateAssert (\<lambda>s. \<not> archOverlap s inRange) [];
haskell_assert (canonicalAddressAssert x4) [];
freeRef <- return (x4 + PPtr (fromIntegral totalObjectSize));
updateFreeIndex x1 (getFreeIndex x3 freeRef);
createNewObjects x5 x1 x7 x4 x6 x8
od
odE \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; s = sa\<rbrakk> \<Longrightarrow> ?Q12 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa proof (prove)
goal (2 subgoals):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace> doE y <- whenE x2 (resetUntypedCap x1);
liftE (do y <- stateAssert (\<lambda>s. \<not> cNodeOverlap (gsCNodes s) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1)) [];
y <- stateAssert (\<lambda>s. \<not> archOverlap s (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1)) [];
y <- updateFreeIndex x1 (getFreeIndex x3 (x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6))));
createNewObjects x5 x1 x7 x4 x6 x8
od)
odE \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; s = sa\<rbrakk> \<Longrightarrow> ?Q12 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa proof (prove)
goal (2 subgoals):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace> whenE x2 (resetUntypedCap x1) \<lbrace>\<lambda>y sa. \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> vs_valid_duplicates' (ksPSpace sa) \<and> (pspace_no_overlap' x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx y () ()) sa \<and> valid_pspace' sa \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) x1 sa) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> K (range_cover x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx y () ()) (getObjectSize x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28)) sa\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; s = sa\<rbrakk> \<Longrightarrow> ?Q12 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa proof (prove)
goal (4 subgoals):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace> whenE x2 (resetUntypedCap x1) \<lbrace>?Q48 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace>, \<lbrace>?E48 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace>
 2. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; ?Q48 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv sa\<rbrakk> \<Longrightarrow> \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> vs_valid_duplicates' (ksPSpace sa) \<and> (pspace_no_overlap' x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) sa \<and> valid_pspace' sa \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) x1 sa) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> K (range_cover x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) (getObjectSize x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28)) sa
 3. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx e sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; ?E48 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx e sa\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace sa)
 4. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; s = sa\<rbrakk> \<Longrightarrow> ?Q12 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa proof (prove)
goal (5 subgoals):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8\<rbrakk> \<Longrightarrow> \<lbrace>?P52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace> whenE x2 (resetUntypedCap x1) \<lbrace>?Q52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace>, \<lbrace>?E52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace>
 2. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8\<rbrakk> \<Longrightarrow> \<lbrace>?P'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace> whenE x2 (resetUntypedCap x1) \<lbrace>?Q'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace>, \<lbrace>?E'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace>
 3. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (?Q52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv and ?Q'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv) sa\<rbrakk> \<Longrightarrow> \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> vs_valid_duplicates' (ksPSpace sa) \<and> (pspace_no_overlap' x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) sa \<and> valid_pspace' sa \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) x1 sa) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> K (range_cover x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) (getObjectSize x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28)) sa
 4. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx e sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (?E52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx e and ?E'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx e) sa\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace sa)
 5. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; s = sa\<rbrakk> \<Longrightarrow> (?P52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx and ?P'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) sa proof (prove)
goal (4 subgoals):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8\<rbrakk> \<Longrightarrow> \<lbrace>?P'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace> whenE x2 (resetUntypedCap x1) \<lbrace>?Q'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace>, \<lbrace>?E'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace>
 2. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (if x2 then 0 else ?idx55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx))) and ct_active' and pspace_no_overlap' (if x2 then ?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx else ?ptr'55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) and ?Q'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv) sa\<rbrakk> \<Longrightarrow> \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> vs_valid_duplicates' (ksPSpace sa) \<and> (pspace_no_overlap' x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) sa \<and> valid_pspace' sa \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) x1 sa) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> K (range_cover x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) (getObjectSize x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28)) sa
 3. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx e sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (invs' and ?E'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx e) sa\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace sa)
 4. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; s = sa\<rbrakk> \<Longrightarrow> (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?idx55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx))) and ct_active' and K (\<exists>ptr_base ty us slots. ui = Invocations_H.untyped_invocation.Retype x1 x2 ptr_base (?ptr'55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) ty us slots (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx)) and ?P'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) sa proof (prove)
goal (4 subgoals):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace> resetUntypedCap x1 \<lbrace>?Q'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace>, \<lbrace>?E'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace>
 2. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (if x2 then 0 else ?idx55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx))) and ct_active' and pspace_no_overlap' (if x2 then ?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx else ?ptr'55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) and ?Q'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv) sa\<rbrakk> \<Longrightarrow> \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> vs_valid_duplicates' (ksPSpace sa) \<and> (pspace_no_overlap' x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) sa \<and> valid_pspace' sa \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) x1 sa) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> K (range_cover x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) (getObjectSize x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28)) sa
 3. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx e sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (invs' and ?E'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx e) sa\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace sa)
 4. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; s = sa\<rbrakk> \<Longrightarrow> (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?idx55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx))) and ct_active' and K (\<exists>ptr_base ty us slots. ui = Invocations_H.untyped_invocation.Retype x1 x2 ptr_base (?ptr'55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) ty us slots (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx)) and (if x2 then ?Q56 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx else ?Q'52 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx ())) sa proof (prove)
goal (4 subgoals):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace> resetUntypedCap x1 \<lbrace>\<lambda>_. ?E'60 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx\<rbrace>
 2. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (if x2 then 0 else ?idx55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx))) and ct_active' and pspace_no_overlap' (if x2 then ?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx else ?ptr'55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) and ?E'60 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) sa\<rbrakk> \<Longrightarrow> \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> vs_valid_duplicates' (ksPSpace sa) \<and> (pspace_no_overlap' x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) sa \<and> valid_pspace' sa \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) x1 sa) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> K (range_cover x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) (getObjectSize x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28)) sa
 3. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx e sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (invs' and ?E'60 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) sa\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace sa)
 4. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; s = sa\<rbrakk> \<Longrightarrow> (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?idx55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx))) and ct_active' and K (\<exists>ptr_base ty us slots. ui = Invocations_H.untyped_invocation.Retype x1 x2 ptr_base (?ptr'55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) ty us slots (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx)) and (if x2 then ?Q56 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx else ?E'60 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (if x2 then 0 else ?idx55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx))) and ct_active' and pspace_no_overlap' (if x2 then ?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx else ?ptr'55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) sa\<rbrakk> \<Longrightarrow> \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> vs_valid_duplicates' (ksPSpace sa) \<and> (pspace_no_overlap' x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) sa \<and> valid_pspace' sa \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) x1 sa) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> K (range_cover x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) (getObjectSize x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28)) sa
 2. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx e sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) sa\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace sa)
 3. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; s = sa\<rbrakk> \<Longrightarrow> (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?idx55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx))) and ct_active' and K (\<exists>ptr_base ty us slots. ui = Invocations_H.untyped_invocation.Retype x1 x2 ptr_base (?ptr'55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) ty us slots (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx)) and (if x2 then (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_objs' and cte_wp_at' (isUntypedCap \<circ> cteCap) x1 else (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))) sa proof (prove)
goal (3 subgoals):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx e sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) sa\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace sa)
 2. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; s = sa\<rbrakk> \<Longrightarrow> (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?idx55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx))) and ct_active' and K (\<exists>ptr_base ty us slots. ui = Invocations_H.untyped_invocation.Retype x1 x2 ptr_base (?ptr'55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) ty us slots (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx)) and (if x2 then (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_objs' and cte_wp_at' (isUntypedCap \<circ> cteCap) x1 else (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))) sa
 3. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (if x2 then 0 else ?idx55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx))) and ct_active' and pspace_no_overlap' (if x2 then ?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx else ?ptr'55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) sa\<rbrakk> \<Longrightarrow> \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> vs_valid_duplicates' (ksPSpace sa) \<and> (pspace_no_overlap' x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) sa \<and> valid_pspace' sa \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) x1 sa) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> K (range_cover x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) (getObjectSize x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; s = sa\<rbrakk> \<Longrightarrow> (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?idx55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx))) and ct_active' and K (\<exists>ptr_base ty us slots. ui = Invocations_H.untyped_invocation.Retype x1 x2 ptr_base (?ptr'55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) ty us slots (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx)) and (if x2 then (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_objs' and cte_wp_at' (isUntypedCap \<circ> cteCap) x1 else (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))) sa
 2. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (if x2 then 0 else ?idx55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx))) and ct_active' and pspace_no_overlap' (if x2 then ?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx else ?ptr'55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) sa\<rbrakk> \<Longrightarrow> \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> vs_valid_duplicates' (ksPSpace sa) \<and> (pspace_no_overlap' x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) sa \<and> valid_pspace' sa \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) x1 sa) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> K (range_cover x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) (getObjectSize x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28)) sa proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' sa; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) sa; invs' sa; vs_valid_duplicates' (ksPSpace sa); invokeUntyped_proofs sa x1 x2 x3 x4 x5 x6 x7 sz idx x8\<rbrakk> \<Longrightarrow> valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap (?dev55 sa x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?ptr55 sa x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 sa x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?idx55 sa x1 x2 x3 x4 x5 x6 x7 x8 sz idx))) sa \<and> x4 = ?ptr'55 sa x1 x2 x3 x4 x5 x6 x7 x8 sz idx \<and> x8 = ?dev55 sa x1 x2 x3 x4 x5 x6 x7 x8 sz idx \<and> (if x2 then (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_objs' and cte_wp_at' (isUntypedCap \<circ> cteCap) x1 else (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) sa
 2. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap (?dev55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (if x2 then 0 else ?idx55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx))) and ct_active' and pspace_no_overlap' (if x2 then ?ptr55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx else ?ptr'55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) (?sz55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) sa\<rbrakk> \<Longrightarrow> \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> vs_valid_duplicates' (ksPSpace sa) \<and> (pspace_no_overlap' x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) sa \<and> valid_pspace' sa \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) x1 sa) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> K (range_cover x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) (getObjectSize x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28)) sa proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8 sz idx sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' sa; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8) (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx)) sa; invs' sa; vs_valid_duplicates' (ksPSpace sa); invokeUntyped_proofs sa x1 x2 x3 x4 x5 x6 x7 sz idx x8\<rbrakk> \<Longrightarrow> x4 = ?ptr'55 sa x1 x2 x3 x4 x5 x6 x7 x8 sz idx \<and> x8 = x8 \<and> (if x2 then (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_objs' and cte_wp_at' (isUntypedCap \<circ> cteCap) x1 else (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) sa
 2. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz (if x2 then 0 else idx))) and ct_active' and pspace_no_overlap' (if x2 then x4 && ~~ mask sz else ?ptr'55 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx) sz and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) sa\<rbrakk> \<Longrightarrow> \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> vs_valid_duplicates' (ksPSpace sa) \<and> (pspace_no_overlap' x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) sa \<and> valid_pspace' sa \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) x1 sa) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> K (range_cover x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) (getObjectSize x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28)) sa proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv sa. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; ct_active' s; \<exists>sza idxa. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sza idxa \<and> capability.UntypedCap x8 (x4 && ~~ mask sz) sz idx = cteCap cte) x1 s \<and> range_cover x4 sza (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 x3 x4 x5 x6 x7 sz idx x8; (invs' and valid_untyped_inv_wcap' ui (Some (capability.UntypedCap x8 (x4 && ~~ mask sz) sz (if x2 then 0 else idx))) and ct_active' and pspace_no_overlap' (if x2 then x4 && ~~ mask sz else x4) sz and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) sa\<rbrakk> \<Longrightarrow> \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1) \<longrightarrow> vs_valid_duplicates' (ksPSpace sa) \<and> (pspace_no_overlap' x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) sa \<and> valid_pspace' sa \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) x1 sa) \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> K (range_cover x4 (?sz44 s x1 x2 x3 x4 x5 x6 x7 x8 sz idx rv () ()) (getObjectSize x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28)) sa proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x4 x5 x6 x7 x8 sz sa idxa cte ctea. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; ct_active' s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 sz idxa x8; invs' sa; ctes_of s x1 = Some cte; ct_active' sa; \<not> x2 \<and> idxa \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; cteCap cte = capability.UntypedCap x8 (x4 && ~~ mask sz) sz idxa; pspace_no_overlap' (if x2 then x4 && ~~ mask sz else x4) sz sa; vs_valid_duplicates' (ksPSpace sa); range_cover x4 sz (APIType_capBits x5 x6) (length x7); ctes_of sa x1 = Some ctea; \<not> x2 \<and> (if x2 then 0 else idxa) \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; cteCap ctea = capability.UntypedCap x8 (x4 && ~~ mask sz) sz (if x2 then 0 else idxa); x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}; x2 \<longrightarrow> descendants_of' x1 (ctes_of sa) = {}; x1 \<notin> set x7; distinct x7; x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6; \<forall>slot\<in>set x7. \<exists>cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.NullCap; x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits; \<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s; \<forall>slot\<in>set x7. \<exists>cte. ctes_of sa slot = Some cte \<and> cteCap cte = capability.NullCap; sch_act_simple s; \<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot sa; sch_act_simple sa; x7 \<noteq> []; x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5; APIType_capBits x5 x6 \<le> maxUntypedSizeBits; \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1); \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1)\<rbrakk> \<Longrightarrow> pspace_no_overlap' x4 (?sz44 s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8 sz idxa () () ()) sa \<and> valid_pspace' sa \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> range_cover x4 (?sz44 s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8 sz idxa () () ()) (APIType_capBits x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x4 x5 x6 x7 x8 sz sa idxa cte ctea. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; ct_active' s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 sz idxa x8; invs' sa; ctes_of s x1 = Some cte; ct_active' sa; \<not> x2 \<and> idxa \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; cteCap cte = capability.UntypedCap x8 (x4 && ~~ mask sz) sz idxa; pspace_no_overlap' (if x2 then x4 && ~~ mask sz else x4) sz sa; vs_valid_duplicates' (ksPSpace sa); range_cover x4 sz (APIType_capBits x5 x6) (length x7); ctes_of sa x1 = Some ctea; \<not> x2 \<and> (if x2 then 0 else idxa) \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; cteCap ctea = capability.UntypedCap x8 (x4 && ~~ mask sz) sz (if x2 then 0 else idxa); x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}; x2 \<longrightarrow> descendants_of' x1 (ctes_of sa) = {}; x1 \<notin> set x7; distinct x7; x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6; \<forall>slot\<in>set x7. \<exists>cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.NullCap; x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits; \<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s; \<forall>slot\<in>set x7. \<exists>cte. ctes_of sa slot = Some cte \<and> cteCap cte = capability.NullCap; sch_act_simple s; \<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot sa; sch_act_simple sa; x7 \<noteq> []; x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5; APIType_capBits x5 x6 \<le> maxUntypedSizeBits; \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1); \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1); x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28\<rbrakk> \<Longrightarrow> pspace_no_overlap' x4 (?sz44 s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8 sz idxa () () ()) sa \<and> valid_pspace' sa \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> range_cover x4 (?sz44 s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8 sz idxa () () ()) (APIType_capBits x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x4 x5 x6 x7 x8 sz sa idxa cte ctea. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; ct_active' s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 sz idxa x8; invs' sa; ctes_of s x1 = Some cte; ct_active' sa; \<not> x2 \<and> idxa \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; cteCap cte = capability.UntypedCap x8 (x4 && ~~ mask sz) sz idxa; pspace_no_overlap' (if x2 then x4 && ~~ mask sz else x4) sz sa; vs_valid_duplicates' (ksPSpace sa); range_cover x4 sz (APIType_capBits x5 x6) (length x7); ctes_of sa x1 = Some ctea; \<not> x2 \<and> (if x2 then 0 else idxa) \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; cteCap ctea = capability.UntypedCap x8 (x4 && ~~ mask sz) sz (if x2 then 0 else idxa); x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}; x2 \<longrightarrow> descendants_of' x1 (ctes_of sa) = {}; x1 \<notin> set x7; distinct x7; x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6; \<forall>slot\<in>set x7. \<exists>cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.NullCap; x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits; \<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s; \<forall>slot\<in>set x7. \<exists>cte. ctes_of sa slot = Some cte \<and> cteCap cte = capability.NullCap; sch_act_simple s; \<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot sa; sch_act_simple sa; x7 \<noteq> []; x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5; APIType_capBits x5 x6 \<le> maxUntypedSizeBits; \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1); \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1); x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28; x4 \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_no_overlap' x4 (?sz44 s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8 sz idxa () () ()) sa \<and> valid_pspace' sa \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> is_aligned (armKSGlobalPD (ksArchState sa)) pdBits \<and> range_cover x4 (?sz44 s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8 sz idxa () () ()) (APIType_capBits x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x4 x5 x6 x7 x8 sz sa idxa cte ctea. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; ct_active' s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 sz idxa x8; invs' sa; ctes_of s x1 = Some cte; ct_active' sa; \<not> x2 \<and> idxa \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; cteCap cte = capability.UntypedCap x8 (x4 && ~~ mask sz) sz idxa; pspace_no_overlap' (if x2 then x4 && ~~ mask sz else x4) sz sa; vs_valid_duplicates' (ksPSpace sa); range_cover x4 sz (APIType_capBits x5 x6) (length x7); ctes_of sa x1 = Some ctea; \<not> x2 \<and> (if x2 then 0 else idxa) \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; cteCap ctea = capability.UntypedCap x8 (x4 && ~~ mask sz) sz (if x2 then 0 else idxa); x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}; x2 \<longrightarrow> descendants_of' x1 (ctes_of sa) = {}; x1 \<notin> set x7; distinct x7; x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6; \<forall>slot\<in>set x7. \<exists>cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.NullCap; x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits; \<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s; \<forall>slot\<in>set x7. \<exists>cte. ctes_of sa slot = Some cte \<and> cteCap cte = capability.NullCap; sch_act_simple s; \<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot sa; sch_act_simple sa; x7 \<noteq> []; x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5; APIType_capBits x5 x6 \<le> maxUntypedSizeBits; \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1); \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1); x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28; x4 \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_no_overlap' x4 (?sz44 s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8 sz idxa () () ()) sa \<and> valid_pspace' sa \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> valid_arch_state' sa \<and> range_cover x4 (?sz44 s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8 sz idxa () () ()) (APIType_capBits x5 x6) (length x7) \<and> x4 \<noteq> 0 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x4 x5 x6 x7 x8 sz sa idxa cte ctea. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; ct_active' s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 sz idxa x8; invs' sa; ctes_of s x1 = Some cte; ct_active' sa; \<not> x2 \<and> idxa \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; cteCap cte = capability.UntypedCap x8 (x4 && ~~ mask sz) sz idxa; pspace_no_overlap' (if x2 then x4 && ~~ mask sz else x4) sz sa; vs_valid_duplicates' (ksPSpace sa); range_cover x4 sz (APIType_capBits x5 x6) (length x7); ctes_of sa x1 = Some ctea; \<not> x2 \<and> (if x2 then 0 else idxa) \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; cteCap ctea = capability.UntypedCap x8 (x4 && ~~ mask sz) sz (if x2 then 0 else idxa); x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}; x2 \<longrightarrow> descendants_of' x1 (ctes_of sa) = {}; x1 \<notin> set x7; distinct x7; x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6; \<forall>slot\<in>set x7. \<exists>cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.NullCap; x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits; \<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s; \<forall>slot\<in>set x7. \<exists>cte. ctes_of sa slot = Some cte \<and> cteCap cte = capability.NullCap; sch_act_simple s; \<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot sa; sch_act_simple sa; x7 \<noteq> []; x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5; APIType_capBits x5 x6 \<le> maxUntypedSizeBits; \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1); \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1); x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28; x4 \<noteq> 0; valid_cap' (capability.UntypedCap x8 (x4 && ~~ mask sz) sz idxa) s\<rbrakk> \<Longrightarrow> pspace_no_overlap' x4 (?sz44 s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8 sz idxa () () ()) sa \<and> valid_pspace' sa \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> valid_arch_state' sa \<and> range_cover x4 (?sz44 s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8 sz idxa () () ()) (APIType_capBits x5 x6) (length x7) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x4 x5 x6 x7 x8 sz sa idxa cte ctea. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; ct_active' s; invs' s; vs_valid_duplicates' (ksPSpace s); invokeUntyped_proofs s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 sz idxa x8; invs' sa; ctes_of s x1 = Some cte; ct_active' sa; \<not> x2 \<and> idxa \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; cteCap cte = capability.UntypedCap x8 (x4 && ~~ mask sz) sz idxa; pspace_no_overlap' (if x2 then x4 && ~~ mask sz else x4) sz sa; vs_valid_duplicates' (ksPSpace sa); range_cover x4 sz (APIType_capBits x5 x6) (length x7); ctes_of sa x1 = Some ctea; \<not> x2 \<and> (if x2 then 0 else idxa) \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; cteCap ctea = capability.UntypedCap x8 (x4 && ~~ mask sz) sz (if x2 then 0 else idxa); x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}; x2 \<longrightarrow> descendants_of' x1 (ctes_of sa) = {}; x1 \<notin> set x7; distinct x7; x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6; \<forall>slot\<in>set x7. \<exists>cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.NullCap; x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits; \<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot s; \<forall>slot\<in>set x7. \<exists>cte. ctes_of sa slot = Some cte \<and> cteCap cte = capability.NullCap; sch_act_simple s; \<forall>slot\<in>set x7. ex_cte_cap_wp_to' (\<lambda>_. True) slot sa; sch_act_simple sa; x7 \<noteq> []; x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5; APIType_capBits x5 x6 \<le> maxUntypedSizeBits; \<not> cNodeOverlap (gsCNodes sa) (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1); \<not> archOverlap sa (\<lambda>x. x4 \<le> x \<and> x \<le> x4 + word_of_nat (shiftL (length x7) (APIType_capBits x5 x6)) - 1); x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x6 < 28; x4 \<noteq> 0; sz < word_bits; valid_untyped' x8 (x4 && ~~ mask sz) sz idxa s; x4 && ~~ mask sz \<noteq> 0; minUntypedSizeBits \<le> sz; sz \<le> maxUntypedSizeBits; idxa \<le> 2 ^ sz; is_aligned (word_of_nat idxa) minUntypedSizeBits\<rbrakk> \<Longrightarrow> pspace_no_overlap' x4 (?sz44 s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8 sz idxa () () ()) sa \<and> valid_pspace' sa \<and> pspace_aligned' sa \<and> pspace_distinct' sa \<and> valid_arch_state' sa \<and> range_cover x4 (?sz44 s x1 x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8 sz idxa () () ()) (APIType_capBits x5 x6) (length x7) proof (prove)
goal:
No subgoals!