theory Retype_AC

lemma invoke_untyped_pas_refined:
  "\<lbrace>pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui
                    and ct_active and K (authorised_untyped_inv aag ui)\<rbrace>
   invoke_untyped ui
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_pre) apply (rule_tac Q="\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs
                                          and valid_arch_state and pas_cur_domain aag" in hoare_strengthen_post) apply (rule invoke_untyped_Q) apply (rule hoare_pre, wp create_cap_pas_refined) apply (clarsimp simp: authorised_untyped_inv_def
                              range_cover.aligned ptr_range_def[symmetric]
                              retype_addrs_aligned_range_cover) apply (clarsimp simp: cte_wp_at_caps_of_state
                              is_cap_simps ptr_range_def[symmetric]) apply (frule cap_cur_auth_caps_of_state
                     [where cap="UntypedCap dev p sz idx" for dev p sz idx], simp+) apply (clarsimp simp add: aag_cap_auth_def ptr_range_def[symmetric]
                                  pas_refined_all_auth_is_owns) apply blast apply (wpsimp wp: init_arch_objects_pas_refined init_arch_objects_invs_from_restricted
              | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state)+ apply (clarsimp simp: retype_addrs_aligned_range_cover
                             cte_wp_at_caps_of_state) apply (rule context_conjI, clarsimp) apply (drule valid_global_refsD[rotated 2]) apply (clarsimp simp: post_retype_invs_def split: if_split_asm) apply (erule caps_of_state_cteD) apply (erule notE, erule subsetD[rotated]) apply (rule order_trans, erule retype_addrs_subset_ptr_bits) apply (simp add: field_simps word_and_le2) apply blast apply (rule hoare_name_pre_state, clarsimp) apply (rule hoare_pre, wp retype_region_pas_refined) apply (rule_tac Q="\<lambda>rv. post_retype_invs tp rv and pas_cur_domain aag" in hoare_strengthen_post) apply (wp retype_region_post_retype_invs_spec) apply (clarsimp simp: post_retype_invs_def invs_def valid_state_def valid_pspace_def split: if_splits) apply (clarsimp simp: authorised_untyped_inv_def) apply (strengthen range_cover_le[mk_strg I E], simp) apply (intro conjI) apply (intro conjI exI;
               (erule cte_wp_at_weakenE)?,
               clarsimp simp: field_simps word_and_le2) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (erule caps_region_kernel_window_imp) apply clarsimp apply clarsimp apply (fastforce simp: word_and_le2) apply (fastforce simp: cte_wp_at_caps_of_state) apply (rule hoare_pre, wp set_cap_pas_refined) apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps) apply (cases ui,
            clarsimp simp: authorised_untyped_inv_def caps_pas_cap_cur_auth_UntypedCap_idx_dev) apply (wp reset_untyped_cap_valid_vspace_objs reset_untyped_cap_valid_arch_state) apply clarsimp apply (cases ui, clarsimp) apply (force simp: descendants_range_def cte_wp_at_caps_of_state authorised_untyped_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active and K (authorised_untyped_inv aag ui)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q2\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q2\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 2. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (7 subgoals):
 1. \<And>tp sz cref slot oref reset ptr us slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>invs and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_range (default_cap tp oref us dev) \<subseteq> untyped_range c \<and> {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c) slot and cte_wp_at ((=) NullCap) cref and K (cref \<in> set slots \<and> oref \<in> set (retype_addrs ptr tp (length slots) us)) and K (range_cover ptr sz (obj_bits_api tp us) (length slots))\<rbrace> create_cap tp us slot dev (cref, oref) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 2. \<And>tp slot reset sz slots ptr n us refs dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag and post_retype_invs tp refs and cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot and K (refs = retype_addrs ptr tp n us \<and> range_cover ptr sz (obj_bits_api tp us) n)\<rbrace> init_arch_objects tp ptr n us refs \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (7 subgoals):
 1. \<And>tp sz cref slot oref reset ptr us slots dev s. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev; (invs and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_range (default_cap tp oref us dev) \<subseteq> untyped_range c \<and> {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c) slot and cte_wp_at ((=) NullCap) cref and K (cref \<in> set slots \<and> oref \<in> set (retype_addrs ptr tp (length slots) us)) and K (range_cover ptr sz (obj_bits_api tp us) (length slots))) s\<rbrakk> \<Longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (tp \<noteq> ArchObject ASIDPoolObj \<and> is_subject aag (fst slot) \<and> is_subject aag (fst (fst (cref, oref))) \<and> (\<forall>x\<in>ptr_range (snd (cref, oref)) (obj_bits_api tp us). is_subject aag x) \<and> is_aligned (snd (cref, oref)) (obj_bits_api tp us))) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_cur_domain aag s
 2. \<And>tp slot reset sz slots ptr n us refs dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag and post_retype_invs tp refs and cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot and K (refs = retype_addrs ptr tp n us \<and> range_cover ptr sz (obj_bits_api tp us) n)\<rbrace> init_arch_objects tp ptr n us refs \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (7 subgoals):
 1. \<And>tp sz a b aa ba oref reset ptr us slots dev s x. \<lbrakk>ui = Retype (aa, ba) reset (ptr && ~~ mask sz) ptr tp us slots dev; is_subject aag aa; invs s; 0 < word_of_nat (length slots); pas_refined aag s; \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; pspace_aligned s; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; valid_vspace_objs s; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x); valid_arch_state s; pas_cur_domain aag s; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_range (default_cap tp oref us dev) \<subseteq> untyped_range c \<and> ptr_range oref (obj_bits_api tp us) \<subseteq> untyped_range c) (aa, ba) s; cte_wp_at ((=) NullCap) (a, b) s; (a, b) \<in> set slots; oref \<in> set (retype_addrs ptr tp (length slots) us); range_cover ptr sz (obj_bits_api tp us) (length slots); x \<in> ptr_range oref (obj_bits_api tp us)\<rbrakk> \<Longrightarrow> is_subject aag x
 2. \<And>tp slot reset sz slots ptr n us refs dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag and post_retype_invs tp refs and cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot and K (refs = retype_addrs ptr tp n us \<and> range_cover ptr sz (obj_bits_api tp us) n)\<rbrace> init_arch_objects tp ptr n us refs \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (7 subgoals):
 1. \<And>tp sz a b aa ba oref reset ptr us slots dev s x deva r bits f. \<lbrakk>ui = Retype (aa, ba) reset (ptr && ~~ mask sz) ptr tp us slots dev; is_subject aag aa; invs s; 0 < word_of_nat (length slots); pas_refined aag s; \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; pspace_aligned s; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; valid_vspace_objs s; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x); valid_arch_state s; pas_cur_domain aag s; caps_of_state s (a, b) = Some NullCap; (a, b) \<in> set slots; oref \<in> set (retype_addrs ptr tp (length slots) us); range_cover ptr sz (obj_bits_api tp us) (length slots); x \<in> ptr_range oref (obj_bits_api tp us); caps_of_state s (aa, ba) = Some (UntypedCap deva r bits f); cap_range (default_cap tp oref us dev) \<subseteq> ptr_range r bits; ptr_range oref (obj_bits_api tp us) \<subseteq> ptr_range r bits\<rbrakk> \<Longrightarrow> is_subject aag x
 2. \<And>tp slot reset sz slots ptr n us refs dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag and post_retype_invs tp refs and cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot and K (refs = retype_addrs ptr tp n us \<and> range_cover ptr sz (obj_bits_api tp us) n)\<rbrace> init_arch_objects tp ptr n us refs \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (7 subgoals):
 1. \<And>tp sz a b aa ba oref reset ptr us slots dev s x deva r bits f. \<lbrakk>ui = Retype (aa, ba) reset (ptr && ~~ mask sz) ptr tp us slots dev; is_subject aag aa; invs s; 0 < word_of_nat (length slots); pas_refined aag s; \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; pspace_aligned s; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; valid_vspace_objs s; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x); valid_arch_state s; pas_cur_domain aag s; caps_of_state s (a, b) = Some NullCap; (a, b) \<in> set slots; oref \<in> set (retype_addrs ptr tp (length slots) us); range_cover ptr sz (obj_bits_api tp us) (length slots); x \<in> ptr_range oref (obj_bits_api tp us); caps_of_state s (aa, ba) = Some (UntypedCap deva r bits f); cap_range (default_cap tp oref us dev) \<subseteq> ptr_range r bits; ptr_range oref (obj_bits_api tp us) \<subseteq> ptr_range r bits; pas_cap_cur_auth aag (UntypedCap deva r bits f)\<rbrakk> \<Longrightarrow> is_subject aag x
 2. \<And>tp slot reset sz slots ptr n us refs dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag and post_retype_invs tp refs and cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot and K (refs = retype_addrs ptr tp n us \<and> range_cover ptr sz (obj_bits_api tp us) n)\<rbrace> init_arch_objects tp ptr n us refs \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (7 subgoals):
 1. \<And>tp sz a b aa ba oref reset ptr us slots dev s x deva r bits f. \<lbrakk>ui = Retype (aa, ba) reset (ptr && ~~ mask sz) ptr tp us slots dev; is_subject aag aa; invs s; 0 < word_of_nat (length slots); pas_refined aag s; \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; pspace_aligned s; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; valid_vspace_objs s; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x); valid_arch_state s; pas_cur_domain aag s; caps_of_state s (a, b) = Some NullCap; (a, b) \<in> set slots; oref \<in> set (retype_addrs ptr tp (length slots) us); range_cover ptr sz (obj_bits_api tp us) (length slots); x \<in> ptr_range oref (obj_bits_api tp us); caps_of_state s (aa, ba) = Some (UntypedCap deva r bits f); cap_range (default_cap tp oref us dev) \<subseteq> ptr_range r bits; ptr_range oref (obj_bits_api tp us) \<subseteq> ptr_range r bits; \<forall>x\<in>ptr_range r bits. is_subject aag x; cap_links_asid_slot aag (pasSubject aag) (UntypedCap deva r bits f); cap_links_irq aag (pasSubject aag) (UntypedCap deva r bits f)\<rbrakk> \<Longrightarrow> is_subject aag x
 2. \<And>tp slot reset sz slots ptr n us refs dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag and post_retype_invs tp refs and cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot and K (refs = retype_addrs ptr tp n us \<and> range_cover ptr sz (obj_bits_api tp us) n)\<rbrace> init_arch_objects tp ptr n us refs \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (6 subgoals):
 1. \<And>tp slot reset sz slots ptr n us refs dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag and post_retype_invs tp refs and cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot and K (refs = retype_addrs ptr tp n us \<and> range_cover ptr sz (obj_bits_api tp us) n)\<rbrace> init_arch_objects tp ptr n us refs \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 2. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 6. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (6 subgoals):
 1. \<And>tp a b reset sz slots ptr n us dev s. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) s; range_cover ptr sz (obj_bits_api tp us) n\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (retype_addrs ptr tp n us). x \<notin> global_refs s) \<and> (\<forall>ref\<in>set (retype_addrs ptr tp n us). is_aligned ref (obj_bits_api tp us)) \<and> global_refs s \<inter> set (retype_addrs ptr tp n us) = {} \<and> (\<forall>ref\<in>set (retype_addrs ptr tp n us). is_aligned ref (obj_bits_api tp us))
 2. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 6. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (6 subgoals):
 1. \<And>tp a b reset sz slots ptr n us dev s idx. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (retype_addrs ptr tp n us). x \<notin> global_refs s) \<and> global_refs s \<inter> set (retype_addrs ptr tp n us) = {}
 2. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 6. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (7 subgoals):
 1. \<And>tp a b reset sz slots ptr n us dev s idx x. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); x \<in> set (retype_addrs ptr tp n us); x \<in> global_refs s\<rbrakk> \<Longrightarrow> False
 2. \<And>tp a b reset sz slots ptr n us dev s idx. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); \<forall>x\<in>set (retype_addrs ptr tp n us). x \<notin> global_refs s\<rbrakk> \<Longrightarrow> global_refs s \<inter> set (retype_addrs ptr tp n us) = {}
 3. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (9 subgoals):
 1. \<And>tp a b reset sz slots ptr n us dev s idx x. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); x \<in> set (retype_addrs ptr tp n us)\<rbrakk> \<Longrightarrow> valid_global_refs s
 2. \<And>tp a b reset sz slots ptr n us dev s idx x. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); x \<in> set (retype_addrs ptr tp n us)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap237 tp a b reset sz slots ptr n us dev s idx x)) (?ptr237 tp a b reset sz slots ptr n us dev s idx x) s
 3. \<And>tp a b reset sz slots ptr n us dev s idx x. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); x \<in> set (retype_addrs ptr tp n us); x \<notin> cap_range (?cap237 tp a b reset sz slots ptr n us dev s idx x)\<rbrakk> \<Longrightarrow> False
 4. \<And>tp a b reset sz slots ptr n us dev s idx. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); \<forall>x\<in>set (retype_addrs ptr tp n us). x \<notin> global_refs s\<rbrakk> \<Longrightarrow> global_refs s \<inter> set (retype_addrs ptr tp n us) = {}
 5. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 7. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 8. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 9. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (8 subgoals):
 1. \<And>tp a b reset sz slots ptr n us dev s idx x. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); x \<in> set (retype_addrs ptr tp n us)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap237 tp a b reset sz slots ptr n us dev s idx x)) (?ptr237 tp a b reset sz slots ptr n us dev s idx x) s
 2. \<And>tp a b reset sz slots ptr n us dev s idx x. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); x \<in> set (retype_addrs ptr tp n us); x \<notin> cap_range (?cap237 tp a b reset sz slots ptr n us dev s idx x)\<rbrakk> \<Longrightarrow> False
 3. \<And>tp a b reset sz slots ptr n us dev s idx. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); \<forall>x\<in>set (retype_addrs ptr tp n us). x \<notin> global_refs s\<rbrakk> \<Longrightarrow> global_refs s \<inter> set (retype_addrs ptr tp n us) = {}
 4. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 7. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 8. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (7 subgoals):
 1. \<And>tp a b reset sz slots ptr n us dev s idx x. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); x \<in> set (retype_addrs ptr tp n us); x \<notin> cap_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> False
 2. \<And>tp a b reset sz slots ptr n us dev s idx. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); \<forall>x\<in>set (retype_addrs ptr tp n us). x \<notin> global_refs s\<rbrakk> \<Longrightarrow> global_refs s \<inter> set (retype_addrs ptr tp n us) = {}
 3. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (7 subgoals):
 1. \<And>tp a b reset sz slots ptr n us dev s idx x. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> set (retype_addrs ptr tp n us) \<subseteq> cap_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)
 2. \<And>tp a b reset sz slots ptr n us dev s idx. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); \<forall>x\<in>set (retype_addrs ptr tp n us). x \<notin> global_refs s\<rbrakk> \<Longrightarrow> global_refs s \<inter> set (retype_addrs ptr tp n us) = {}
 3. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (7 subgoals):
 1. \<And>tp a b reset sz slots ptr n us dev s idx x. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> up_aligned_area ptr sz \<subseteq> cap_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)
 2. \<And>tp a b reset sz slots ptr n us dev s idx. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); \<forall>x\<in>set (retype_addrs ptr tp n us). x \<notin> global_refs s\<rbrakk> \<Longrightarrow> global_refs s \<inter> set (retype_addrs ptr tp n us) = {}
 3. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (6 subgoals):
 1. \<And>tp a b reset sz slots ptr n us dev s idx. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; post_retype_invs tp (retype_addrs ptr tp n us) s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); \<forall>x\<in>set (retype_addrs ptr tp n us). x \<notin> global_refs s\<rbrakk> \<Longrightarrow> global_refs s \<inter> set (retype_addrs ptr tp n us) = {}
 2. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 6. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (5 subgoals):
 1. \<And>ptr us tp slot reset sz slots dev. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 2. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 5. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (5 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev s. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) s; pspace_no_overlap (up_aligned_area ptr sz) s; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s; caps_no_overlap ptr sz s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_ x. pas_refined aag x \<and> pspace_aligned x \<and> valid_vspace_objs x \<and> valid_arch_state x \<and> pas_cur_domain aag x\<rbrace>
 2. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 5. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (6 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev s. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) s; pspace_no_overlap (up_aligned_area ptr sz) s; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s; caps_no_overlap ptr sz s\<rbrakk> \<Longrightarrow> \<lbrace>?P'329 ptr us tp a b reset sz slots dev s\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>rv s. pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_cur_domain aag s\<rbrace>
 2. \<And>ptr us tp a b reset sz slots dev s sa. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) s; pspace_no_overlap (up_aligned_area ptr sz) s; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s; caps_no_overlap ptr sz s; s = sa\<rbrakk> \<Longrightarrow> (pas_refined aag and invs and pas_cur_domain aag and caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} and caps_no_overlap ptr (?sz330 ptr us tp a b reset sz slots dev s) and pspace_no_overlap (up_aligned_area ptr (?sz330 ptr us tp a b reset sz slots dev s)) and (\<lambda>sa. \<exists>sl. cte_wp_at (\<lambda>c. up_aligned_area ptr (?sz330 ptr us tp a b reset sz slots dev s) \<subseteq> cap_range c \<and> cap_is_device c = dev) sl sa) and K (range_cover ptr (?sz330 ptr us tp a b reset sz slots dev s) (obj_bits_api tp us) (length slots)) and K (\<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x) and K (tp = CapTableObject \<longrightarrow> 0 < us)) sa \<and> ?P'329 ptr us tp a b reset sz slots dev s sa
 3. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 6. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (7 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev s. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) s; pspace_no_overlap (up_aligned_area ptr sz) s; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s; caps_no_overlap ptr sz s\<rbrakk> \<Longrightarrow> \<lbrace>?P'329 ptr us tp a b reset sz slots dev s\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>rv. post_retype_invs tp rv and pas_cur_domain aag\<rbrace>
 2. \<And>ptr us tp a b reset sz slots dev s rv sa. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) s; pspace_no_overlap (up_aligned_area ptr sz) s; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s; caps_no_overlap ptr sz s; (post_retype_invs tp rv and pas_cur_domain aag) sa\<rbrakk> \<Longrightarrow> pspace_aligned sa \<and> valid_vspace_objs sa \<and> valid_arch_state sa \<and> pas_cur_domain aag sa
 3. \<And>ptr us tp a b reset sz slots dev s sa. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) s; pspace_no_overlap (up_aligned_area ptr sz) s; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s; caps_no_overlap ptr sz s; s = sa\<rbrakk> \<Longrightarrow> (pas_refined aag and invs and pas_cur_domain aag and caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} and caps_no_overlap ptr (?sz330 ptr us tp a b reset sz slots dev s) and pspace_no_overlap (up_aligned_area ptr (?sz330 ptr us tp a b reset sz slots dev s)) and (\<lambda>sa. \<exists>sl. cte_wp_at (\<lambda>c. up_aligned_area ptr (?sz330 ptr us tp a b reset sz slots dev s) \<subseteq> cap_range c \<and> cap_is_device c = dev) sl sa) and K (range_cover ptr (?sz330 ptr us tp a b reset sz slots dev s) (obj_bits_api tp us) (length slots)) and K (\<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x) and K (tp = CapTableObject \<longrightarrow> 0 < us)) sa \<and> ?P'329 ptr us tp a b reset sz slots dev s sa
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (6 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev s rv sa. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) s; pspace_no_overlap (up_aligned_area ptr sz) s; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s; caps_no_overlap ptr sz s; (post_retype_invs tp rv and pas_cur_domain aag) sa\<rbrakk> \<Longrightarrow> pspace_aligned sa \<and> valid_vspace_objs sa \<and> valid_arch_state sa \<and> pas_cur_domain aag sa
 2. \<And>ptr us tp a b reset sz slots dev s sa. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) s; pspace_no_overlap (up_aligned_area ptr sz) s; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s; caps_no_overlap ptr sz s; s = sa\<rbrakk> \<Longrightarrow> (pas_refined aag and invs and pas_cur_domain aag and caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} and caps_no_overlap ptr (?sz330 ptr us tp a b reset sz slots dev s) and pspace_no_overlap (up_aligned_area ptr (?sz330 ptr us tp a b reset sz slots dev s)) and (\<lambda>sa. \<exists>sl. cte_wp_at (\<lambda>c. up_aligned_area ptr (?sz330 ptr us tp a b reset sz slots dev s) \<subseteq> cap_range c \<and> cap_is_device c = dev) sl sa) and K (range_cover ptr (?sz330 ptr us tp a b reset sz slots dev s) (obj_bits_api tp us) (length slots)) and K (\<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x) and K (tp = CapTableObject \<longrightarrow> 0 < us)) sa \<and> (invs and caps_no_overlap ptr (?sz336 ptr us tp a b reset sz slots dev s) and pspace_no_overlap (up_aligned_area ptr (?sz336 ptr us tp a b reset sz slots dev s)) and caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} and region_in_kernel_window {ptr..(ptr && ~~ mask (?sz336 ptr us tp a b reset sz slots dev s)) + 2 ^ ?sz336 ptr us tp a b reset sz slots dev s - 1} and (\<lambda>sa. \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask (?sz336 ptr us tp a b reset sz slots dev s)) (?sz336 ptr us tp a b reset sz slots dev s) idx)) (?slot336 ptr us tp a b reset sz slots dev s) sa) and K (tp = CapTableObject \<longrightarrow> 0 < us) and K (range_cover ptr (?sz336 ptr us tp a b reset sz slots dev s) (obj_bits_api tp us) (length slots))) sa \<and> pas_cur_domain aag sa
 3. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 6. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (5 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev s sa. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) s; pspace_no_overlap (up_aligned_area ptr sz) s; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s; caps_no_overlap ptr sz s; s = sa\<rbrakk> \<Longrightarrow> (pas_refined aag and invs and pas_cur_domain aag and caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} and caps_no_overlap ptr (?sz330 ptr us tp a b reset sz slots dev s) and pspace_no_overlap (up_aligned_area ptr (?sz330 ptr us tp a b reset sz slots dev s)) and (\<lambda>sa. \<exists>sl. cte_wp_at (\<lambda>c. up_aligned_area ptr (?sz330 ptr us tp a b reset sz slots dev s) \<subseteq> cap_range c \<and> cap_is_device c = dev) sl sa) and K (range_cover ptr (?sz330 ptr us tp a b reset sz slots dev s) (obj_bits_api tp us) (length slots)) and K (\<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x) and K (tp = CapTableObject \<longrightarrow> 0 < us)) sa \<and> (invs and caps_no_overlap ptr (?sz336 ptr us tp a b reset sz slots dev s) and pspace_no_overlap (up_aligned_area ptr (?sz336 ptr us tp a b reset sz slots dev s)) and caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} and region_in_kernel_window {ptr..(ptr && ~~ mask (?sz336 ptr us tp a b reset sz slots dev s)) + 2 ^ ?sz336 ptr us tp a b reset sz slots dev s - 1} and (\<lambda>sa. \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask (?sz336 ptr us tp a b reset sz slots dev s)) (?sz336 ptr us tp a b reset sz slots dev s) idx)) (?slot336 ptr us tp a b reset sz slots dev s) sa) and K (tp = CapTableObject \<longrightarrow> 0 < us) and K (range_cover ptr (?sz336 ptr us tp a b reset sz slots dev s) (obj_bits_api tp us) (length slots))) sa \<and> pas_cur_domain aag sa
 2. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 5. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (5 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev sa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> caps_no_overlap ptr (?sz330 ptr us tp a b reset sz slots dev sa) sa \<and> pspace_no_overlap (up_aligned_area ptr (?sz330 ptr us tp a b reset sz slots dev sa)) sa \<and> (\<exists>aa ba. cte_wp_at (\<lambda>c. up_aligned_area ptr (?sz330 ptr us tp a b reset sz slots dev sa) \<subseteq> cap_range c \<and> cap_is_device c = dev) (aa, ba) sa) \<and> range_cover ptr (?sz330 ptr us tp a b reset sz slots dev sa) (obj_bits_api tp us) (length slots) \<and> caps_no_overlap ptr (?sz336 ptr us tp a b reset sz slots dev sa) sa \<and> pspace_no_overlap (up_aligned_area ptr (?sz336 ptr us tp a b reset sz slots dev sa)) sa \<and> region_in_kernel_window {ptr..(ptr && ~~ mask (?sz336 ptr us tp a b reset sz slots dev sa)) + 2 ^ ?sz336 ptr us tp a b reset sz slots dev sa - 1} sa \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask (?sz336 ptr us tp a b reset sz slots dev sa)) (?sz336 ptr us tp a b reset sz slots dev sa) idx)) (?slot336 ptr us tp a b reset sz slots dev sa) sa) \<and> range_cover ptr (?sz336 ptr us tp a b reset sz slots dev sa) (obj_bits_api tp us) (length slots)
 2. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 5. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (5 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev sa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) sa) \<and> region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} sa \<and> (\<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) (?slot336 ptr us tp a b reset sz slots dev sa) sa)
 2. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 5. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (7 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev sa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) sa
 2. \<And>ptr us tp a b reset sz slots dev sa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} sa
 3. \<And>ptr us tp a b reset sz slots dev sa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) (?slot336 ptr us tp a b reset sz slots dev sa) sa
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (6 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev sa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} sa
 2. \<And>ptr us tp a b reset sz slots dev sa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) (?slot336 ptr us tp a b reset sz slots dev sa) sa
 3. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 6. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (6 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev sa idx. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x); caps_of_state sa (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} sa
 2. \<And>ptr us tp a b reset sz slots dev sa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) (?slot336 ptr us tp a b reset sz slots dev sa) sa
 3. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 6. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (7 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev sa idx. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> cap_refs_in_kernel_window sa
 2. \<And>ptr us tp a b reset sz slots dev sa idx. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> cap_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)
 3. \<And>ptr us tp a b reset sz slots dev sa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) (?slot336 ptr us tp a b reset sz slots dev sa) sa
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (6 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev sa idx. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> cap_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)
 2. \<And>ptr us tp a b reset sz slots dev sa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) (?slot336 ptr us tp a b reset sz slots dev sa) sa
 3. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 6. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (6 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev sa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x); ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> ptr
 2. \<And>ptr us tp a b reset sz slots dev sa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) (?slot336 ptr us tp a b reset sz slots dev sa) sa
 3. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 5. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 6. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (5 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev sa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa; pas_refined aag sa; pspace_aligned sa; valid_vspace_objs sa; valid_arch_state sa; pas_cur_domain aag sa; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) sa; pspace_no_overlap (up_aligned_area ptr sz) sa; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; is_subject aag a; 0 < word_of_nat (length slots); \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) (?slot336 ptr us tp a b reset sz slots dev sa) sa
 2. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 4. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 5. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (4 subgoals):
 1. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 2. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (4 subgoals):
 1. \<And>ptr sz idx cref dev s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s \<and> invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref s \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_transferable_in cref s \<and> \<not> Option.is_none (cdt s cref) \<longrightarrow> is_transferable_cap (UntypedCap dev ptr sz idx) \<or> (pasObjectAbs aag (fst $ the $ cdt s cref), Control, pasObjectAbs aag (fst cref)) \<in> pasPolicy aag) and K (aag_cap_auth aag (pasObjectAbs aag (fst cref)) (UntypedCap dev ptr sz idx))) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_cur_domain aag s
 2. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (4 subgoals):
 1. \<And>idx a b dev s deva r bits f. \<lbrakk>authorised_untyped_inv aag ui; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; pas_cur_domain aag s; invs s; case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> (a, b) = slot \<and> dev' = dev; idx \<le> 2 ^ bits; caps_of_state s (a, b) = Some (UntypedCap deva r bits f)\<rbrakk> \<Longrightarrow> aag_cap_auth aag (pasObjectAbs aag a) (UntypedCap dev r bits idx)
 2. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 3. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (3 subgoals):
 1. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q'7\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag\<rbrace>
 2. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'7 s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> (pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s) and K (is_subject aag (fst (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)))) s \<and> pspace_aligned s \<and> (invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s) \<and> (invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s) \<and> pas_cur_domain aag s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> (pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s) and K (is_subject aag (fst (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)))) s \<and> pspace_aligned s \<and> (invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s) \<and> (invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s) \<and> pas_cur_domain aag s) and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and pas_cur_domain aag) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8); ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; pas_refined aag s; pas_cur_domain aag s; invs s; ct_active s; cte_wp_at (\<lambda>c. c = UntypedCap x8 (x4 && ~~ mask sz) sz idx) (a, b) s; range_cover x4 sz (obj_bits_api x5 x6) (length x7); idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. cte_wp_at ((=) NullCap) slot s \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; x5 \<noteq> ArchObject ASIDPoolObj; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5\<rbrakk> \<Longrightarrow> (x2 \<longrightarrow> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (a, b) s) (a, b) s \<and> is_subject aag a \<and> pspace_aligned s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (a, b) s) (a, b) s) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal:
No subgoals!