theory ArchRetype_IF

lemma invoke_untyped_globals_equiv:
  notes blah[simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff
                         atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost
                         atLeastatMost_empty_iff split_paired_Ex
  shows "\<lbrace>globals_equiv st and invs and valid_untyped_inv ui and ct_active\<rbrace>
         invoke_untyped ui
         \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (rule hoare_name_pre_state) apply (rule hoare_pre, rule invoke_untyped_Q) apply (wp create_cap_globals_equiv) apply auto[1] apply (wp init_arch_objects_globals_equiv) apply (clarsimp simp: retype_addrs_aligned_range_cover cte_wp_at_caps_of_state
                  simp del: valid_untyped_inv_wcap.simps) apply (frule valid_global_refsD2) apply (clarsimp simp: post_retype_invs_def split: if_split_asm) apply (drule disjoint_subset2[rotated]) apply (rule order_trans, erule retype_addrs_subset_ptr_bits) apply (simp add: untyped_range_def blah word_and_le2 field_simps) apply (auto simp: global_refs_def post_retype_invs_def split: if_split_asm)[1] apply (rule hoare_pre, wp retype_region_globals_equiv[where slot="slot_of_untyped_inv ui"]) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (strengthen refl) apply simp apply (wp set_cap_globals_equiv) apply auto[1] apply (wp reset_untyped_cap_globals_equiv) apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and invs and valid_untyped_inv ui and ct_active\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s tp sz cref slot oref reset ptr us slots dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>invs and globals_equiv st 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>_. globals_equiv st\<rbrace>
 2. \<And>s tp slot reset sz slots ptr n us refs dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>globals_equiv st 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>_. globals_equiv st\<rbrace>
 3. \<And>s ptr us tp slot reset sz slots dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> globals_equiv st 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>_. globals_equiv st\<rbrace>
 4. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 5. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (6 subgoals):
 1. \<And>s tp sz cref slot oref reset ptr us slots dev sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev; (invs and globals_equiv st 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))) sa\<rbrakk> \<Longrightarrow> (globals_equiv st and valid_global_objs and valid_arch_state) sa
 2. \<And>s tp slot reset sz slots ptr n us refs dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>globals_equiv st 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>_. globals_equiv st\<rbrace>
 3. \<And>s ptr us tp slot reset sz slots dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> globals_equiv st 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>_. globals_equiv st\<rbrace>
 4. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 5. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (5 subgoals):
 1. \<And>s tp slot reset sz slots ptr n us refs dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>globals_equiv st 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>_. globals_equiv st\<rbrace>
 2. \<And>s ptr us tp slot reset sz slots dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> globals_equiv st 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>_. globals_equiv st\<rbrace>
 3. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 4. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (5 subgoals):
 1. \<And>s tp slot reset sz slots ptr n us refs dev sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev; (globals_equiv st 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)) sa\<rbrakk> \<Longrightarrow> (globals_equiv st and (\<lambda>s. arm_global_pd (arch_state s) \<notin> set refs \<and> pspace_aligned s \<and> valid_arch_state s) and K (\<forall>x\<in>set refs. is_aligned x (obj_bits_api tp us))) sa
 2. \<And>s ptr us tp slot reset sz slots dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> globals_equiv st 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>_. globals_equiv st\<rbrace>
 3. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 4. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (5 subgoals):
 1. \<And>s tp a b reset sz slots ptr n us dev sa idx. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; globals_equiv st s; globals_equiv st sa; invs s; post_retype_invs tp (retype_addrs ptr tp n us) sa; valid_untyped_inv (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev) s; ct_active s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state sa (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state sa) \<notin> set (retype_addrs ptr tp n us) \<and> pspace_aligned sa \<and> valid_arch_state sa
 2. \<And>s ptr us tp slot reset sz slots dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> globals_equiv st 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>_. globals_equiv st\<rbrace>
 3. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 4. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (6 subgoals):
 1. \<And>s tp a b reset sz slots ptr n us dev sa idx. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; globals_equiv st s; globals_equiv st sa; invs s; post_retype_invs tp (retype_addrs ptr tp n us) sa; valid_untyped_inv (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev) s; ct_active s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state sa (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> valid_global_refs sa
 2. \<And>s tp a b reset sz slots ptr n us dev sa idx. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; globals_equiv st s; globals_equiv st sa; invs s; post_retype_invs tp (retype_addrs ptr tp n us) sa; valid_untyped_inv (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev) s; ct_active s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state sa (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); global_refs sa \<inter> cap_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) = {}\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state sa) \<notin> set (retype_addrs ptr tp n us) \<and> pspace_aligned sa \<and> valid_arch_state sa
 3. \<And>s ptr us tp slot reset sz slots dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> globals_equiv st 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>_. globals_equiv st\<rbrace>
 4. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 5. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (5 subgoals):
 1. \<And>s tp a b reset sz slots ptr n us dev sa idx. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; globals_equiv st s; globals_equiv st sa; invs s; post_retype_invs tp (retype_addrs ptr tp n us) sa; valid_untyped_inv (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev) s; ct_active s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state sa (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); global_refs sa \<inter> cap_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) = {}\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state sa) \<notin> set (retype_addrs ptr tp n us) \<and> pspace_aligned sa \<and> valid_arch_state sa
 2. \<And>s ptr us tp slot reset sz slots dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> globals_equiv st 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>_. globals_equiv st\<rbrace>
 3. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 4. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (6 subgoals):
 1. \<And>s tp a b reset sz slots ptr n us dev sa idx. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; globals_equiv st s; globals_equiv st sa; invs s; post_retype_invs tp (retype_addrs ptr tp n us) sa; valid_untyped_inv (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev) s; ct_active s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state sa (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> ?B'240 s tp a b reset sz slots ptr n us dev sa idx \<subseteq> cap_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)
 2. \<And>s tp a b reset sz slots ptr n us dev sa idx. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; globals_equiv st s; globals_equiv st sa; invs s; post_retype_invs tp (retype_addrs ptr tp n us) sa; valid_untyped_inv (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev) s; ct_active s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state sa (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); global_refs sa \<inter> ?B'240 s tp a b reset sz slots ptr n us dev sa idx = {}\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state sa) \<notin> set (retype_addrs ptr tp n us) \<and> pspace_aligned sa \<and> valid_arch_state sa
 3. \<And>s ptr us tp slot reset sz slots dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> globals_equiv st 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>_. globals_equiv st\<rbrace>
 4. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 5. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (6 subgoals):
 1. \<And>s tp a b reset sz slots ptr n us dev sa idx. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; globals_equiv st s; globals_equiv st sa; invs s; post_retype_invs tp (retype_addrs ptr tp n us) sa; valid_untyped_inv (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev) s; ct_active s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state sa (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>s tp a b reset sz slots ptr n us dev sa idx. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; globals_equiv st s; globals_equiv st sa; invs s; post_retype_invs tp (retype_addrs ptr tp n us) sa; valid_untyped_inv (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev) s; ct_active s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state sa (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); global_refs sa \<inter> set (retype_addrs ptr tp n us) = {}\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state sa) \<notin> set (retype_addrs ptr tp n us) \<and> pspace_aligned sa \<and> valid_arch_state sa
 3. \<And>s ptr us tp slot reset sz slots dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> globals_equiv st 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>_. globals_equiv st\<rbrace>
 4. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 5. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (5 subgoals):
 1. \<And>s tp a b reset sz slots ptr n us dev sa idx. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; globals_equiv st s; globals_equiv st sa; invs s; post_retype_invs tp (retype_addrs ptr tp n us) sa; valid_untyped_inv (Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev) s; ct_active s; range_cover ptr sz (obj_bits_api tp us) n; caps_of_state sa (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); global_refs sa \<inter> set (retype_addrs ptr tp n us) = {}\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state sa) \<notin> set (retype_addrs ptr tp n us) \<and> pspace_aligned sa \<and> valid_arch_state sa
 2. \<And>s ptr us tp slot reset sz slots dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> globals_equiv st 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>_. globals_equiv st\<rbrace>
 3. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 4. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (4 subgoals):
 1. \<And>s ptr us tp slot reset sz slots dev. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> globals_equiv st 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>_. globals_equiv st\<rbrace>
 2. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 3. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (4 subgoals):
 1. \<And>s ptr us tp slot reset sz slots dev sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev; invs sa \<and> globals_equiv st sa \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot sa \<and> pspace_no_overlap (up_aligned_area ptr sz) sa \<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} sa \<and> caps_no_overlap ptr sz sa\<rbrakk> \<Longrightarrow> (globals_equiv st and invs and (\<lambda>sa. \<exists>i. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask (?sz439 s ptr us tp slot reset sz slots dev)) (?sz439 s ptr us tp slot reset sz slots dev) i) (slot_of_untyped_inv ui) sa \<and> (i \<le> unat (ptr && mask (?sz439 s ptr us tp slot reset sz slots dev)) \<or> pspace_no_overlap (up_aligned_area ptr (?sz439 s ptr us tp slot reset sz slots dev)) sa)) and K (range_cover ptr (?sz439 s ptr us tp slot reset sz slots dev) (obj_bits_api tp us) (length slots) \<and> 0 < length slots)) sa
 2. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 3. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (4 subgoals):
 1. \<And>s ptr us tp a b reset sz slots dev sa sza idx idxa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; globals_equiv st s; invs sa; invs s; globals_equiv st sa; ct_active s; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sza idx); pspace_no_overlap (up_aligned_area ptr sz) sa; caps_of_state sa (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idxa); range_cover ptr sza (obj_bits_api tp us) (length slots); range_cover ptr sz (obj_bits_api tp us) (length slots); idx \<le> unat (ptr && mask sz) \<or> reset \<and> ptr = ptr && ~~ mask sz; tp = CapTableObject \<longrightarrow> 0 < us; ptr && ~~ mask sza = ptr && ~~ mask sz; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; reset \<longrightarrow> descendants_of (a, b) (cdt s) = {}; tp = Untyped \<longrightarrow> untyped_min_bits \<le> us; (a, b) \<notin> set slots; distinct slots; \<forall>slot\<in>set slots. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; tp \<noteq> ArchObject ASIDPoolObj; slots \<noteq> []; dev \<longrightarrow> tp = Untyped \<or> is_frame_type tp\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz = ptr && ~~ mask (?sz439 s ptr us tp (a, b) reset sz slots dev) \<and> sz = ?sz439 s ptr us tp (a, b) reset sz slots dev \<and> (idxa \<le> unat (ptr && mask (?sz439 s ptr us tp (a, b) reset sz slots dev)) \<or> pspace_no_overlap (up_aligned_area ptr (?sz439 s ptr us tp (a, b) reset sz slots dev)) sa) \<and> range_cover ptr (?sz439 s ptr us tp (a, b) reset sz slots dev) (obj_bits_api tp us) (length slots)
 2. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 3. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (4 subgoals):
 1. \<And>s ptr us tp a b reset sz slots dev sa sza idx idxa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; globals_equiv st s; invs sa; invs s; globals_equiv st sa; ct_active s; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sza idx); pspace_no_overlap (up_aligned_area ptr sz) sa; caps_of_state sa (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idxa); range_cover ptr sza (obj_bits_api tp us) (length slots); range_cover ptr sz (obj_bits_api tp us) (length slots); idx \<le> unat (ptr && mask sz) \<or> reset \<and> ptr = ptr && ~~ mask sz; tp = CapTableObject \<longrightarrow> 0 < us; ptr && ~~ mask sza = ptr && ~~ mask sz; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} sa; caps_no_overlap ptr sz sa; reset \<longrightarrow> descendants_of (a, b) (cdt s) = {}; tp = Untyped \<longrightarrow> untyped_min_bits \<le> us; (a, b) \<notin> set slots; distinct slots; \<forall>slot\<in>set slots. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; tp \<noteq> ArchObject ASIDPoolObj; slots \<noteq> []; dev \<longrightarrow> tp = Untyped \<or> is_frame_type tp\<rbrakk> \<Longrightarrow> True \<and> True \<and> (idxa \<le> unat (ptr && mask sz) \<or> pspace_no_overlap (up_aligned_area ptr sz) sa) \<and> range_cover ptr sz (obj_bits_api tp us) (length slots)
 2. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 3. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (3 subgoals):
 1. \<And>s ptr sz idx cref dev. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>\<lambda>x. globals_equiv st 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>_. globals_equiv st\<rbrace>
 2. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (3 subgoals):
 1. \<And>s ptr sz idx cref dev sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; globals_equiv st sa \<and> invs sa \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref sa \<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> (globals_equiv st and valid_global_objs and valid_arch_state) sa
 2. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. (globals_equiv st and invs and valid_untyped_inv ui and ct_active) s \<Longrightarrow> \<lbrace>?Q'5 s\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>sa. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'5 s sa) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>(globals_equiv st and invs and valid_untyped_inv ui and ct_active) s; s = sa\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> (globals_equiv st and invs and cte_wp_at is_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) and ct_active and (\<lambda>s. descendants_of (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) (cdt s) = {})) s) and globals_equiv st and valid_untyped_inv ui and ct_active) sa proof (prove)
goal:
No subgoals!