theory FinalCaps

lemma invoke_untyped_silc_inv:
  "\<lbrace>silc_inv aag st and invs and pas_refined aag and ct_active
                    and valid_untyped_inv ui and K (authorised_untyped_inv aag ui)\<rbrace>
   invoke_untyped ui
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_pre) apply (rule_tac Q="\<lambda>_. silc_inv aag st and
                          cte_wp_at (\<lambda>cp. is_untyped_cap cp
                                          \<longrightarrow> (\<forall>x \<in> untyped_range cp. is_subject aag x))
                                    (case ui of Retype src_slot _ _ _ _ _ _ _ \<Rightarrow> src_slot)"
                in hoare_strengthen_post) apply (rule invoke_untyped_Q) apply (rule hoare_pre, wp create_cap_silc_inv create_cap_pas_refined) apply (clarsimp simp: authorised_untyped_inv_def) apply (auto simp: cte_wp_at_caps_of_state)[1] apply ((wp | simp)+)[1] apply (rule hoare_pre) apply (wp retype_region_silc_inv retype_cte_wp_at | simp)+ apply clarsimp apply (strengthen range_cover_le[mk_strg I E]) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (simp add: invs_valid_pspace) apply (erule ball_subset) apply (simp add: word_and_le2 field_simps) apply (rule hoare_pre) apply (wp set_cap_silc_inv_simple set_cap_cte_wp_at) apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state is_cap_simps
                          split del: if_split cong: if_cong) apply (clarsimp simp: authorised_untyped_inv_def) apply (wp reset_untyped_cap_silc_inv reset_untyped_cap_untyped_cap) apply simp apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state authorised_untyped_inv_def) apply (frule (1) cap_auth_caps_of_state) apply (clarsimp simp: aag_cap_auth_def aag_has_Control_iff_owns) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui and K (authorised_untyped_inv aag ui)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q2\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 2. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 3. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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>silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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> (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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> (silc_inv aag st and K (is_subject aag (fst (fst (cref, oref))) \<and> is_subject aag (snd (cref, oref)) \<and> is_subject aag (fst slot))) s \<and> (cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) and K ((case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<noteq> cref)) 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>silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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> (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (7 subgoals):
 1. \<And>tp sz a b oref reset ptr us slots dev s. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; is_subject aag a; invs s; 0 < word_of_nat (length slots); silc_inv aag st s; \<forall>x\<in>set (retype_addrs ptr tp (length slots) us). is_subject aag x; cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (a, b) s; \<forall>x\<in>{ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1}. is_subject aag x; 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) (a, b) s; tp \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set slots. is_subject aag (fst x); 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)\<rbrakk> \<Longrightarrow> False
 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>silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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> (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 4. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 6. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 7. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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> (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 3. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 5. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 6. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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> (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 2. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 4. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 5. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (6 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>?Q50 ptr us tp slot reset sz slots dev\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 2. \<And>ptr us tp slot reset sz slots dev s. \<lbrakk>authorised_untyped_inv aag ui; ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev; invs s \<and> (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<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} s \<and> caps_no_overlap ptr sz s\<rbrakk> \<Longrightarrow> ?Q50 ptr us tp slot reset sz slots dev s
 3. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 5. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 6. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (5 subgoals):
 1. \<And>ptr us tp slot reset sz slots dev s. \<lbrakk>authorised_untyped_inv aag (Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev); ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev; invs s \<and> silc_inv aag st s \<and> cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) slot s \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<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} s \<and> caps_no_overlap ptr sz s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz56 ptr us tp slot reset sz slots dev) (obj_bits_api tp us) (length slots) \<and> (\<forall>x\<in>up_aligned_area ptr (?sz56 ptr us tp slot reset sz slots dev). is_subject aag x) \<and> pspace_no_overlap (up_aligned_area ptr (?sz57 ptr us tp slot reset sz slots dev)) s \<and> valid_pspace s \<and> range_cover ptr (?sz57 ptr us tp slot reset sz slots dev) (obj_bits_api tp us) (length slots)
 2. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 4. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 5. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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; silc_inv aag st s; cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (a, b) 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> range_cover ptr (?sz56 ptr us tp (a, b) reset sz slots dev) (obj_bits_api tp us) (length slots) \<and> (\<forall>x\<in>up_aligned_area ptr (?sz56 ptr us tp (a, b) reset sz slots dev). is_subject aag x) \<and> pspace_no_overlap (up_aligned_area ptr (?sz57 ptr us tp (a, b) reset sz slots dev)) s \<and> valid_pspace s \<and> range_cover ptr (?sz57 ptr us tp (a, b) reset sz slots dev) (obj_bits_api tp us) (length slots)
 2. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 4. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 5. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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; silc_inv aag st s; cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (a, b) 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> length slots \<le> length slots \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x) \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_pspace s \<and> length slots \<le> length slots
 2. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 4. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 5. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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 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; invs s; silc_inv aag st 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; \<forall>x\<in>{ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}. is_subject aag x; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x) \<and> valid_pspace s
 2. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 4. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 5. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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 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; invs s; silc_inv aag st 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; \<forall>x\<in>{ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}. is_subject aag x; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x
 2. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 4. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 5. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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 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; invs s; silc_inv aag st 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; caps_of_state s (a, b) = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> up_aligned_area ptr sz \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>\<lambda>x. (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 4. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 5. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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. (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 3. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 4. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (5 subgoals):
 1. \<And>ptr sz idx cref dev. authorised_untyped_inv aag ui \<Longrightarrow> \<lbrace>?Q97 ptr sz idx cref dev\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 2. \<And>ptr sz idx cref dev s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (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> 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> ?Q97 ptr sz idx cref dev s
 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 4. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 5. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (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> 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> (silc_inv aag st and cte_wp_at (\<lambda>cp. cap_irqs cp = cap_irqs (UntypedCap dev ptr sz idx) \<and> obj_refs cp = obj_refs (UntypedCap dev ptr sz idx)) cref and K (is_subject aag (fst cref))) s \<and> ((\<lambda>s. if (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) = cref then is_untyped_cap (UntypedCap dev ptr sz idx) \<longrightarrow> (\<forall>x\<in>untyped_range (UntypedCap dev ptr sz idx). is_subject aag x) else cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s) and cte_wp_at (\<lambda>_. True) cref) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 3. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 4. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (4 subgoals):
 1. \<And>idx a b dev s x2 x3 x4 x5 x6 x7 deva r bits f. \<lbrakk>authorised_untyped_inv aag (Retype (a, b) x2 x3 x4 x5 x6 x7 dev); ui = Retype (a, b) x2 x3 x4 x5 x6 x7 dev; silc_inv aag st s; invs s; \<forall>x\<in>{r..r + 2 ^ bits - 1}. is_subject aag x; idx \<le> 2 ^ bits; caps_of_state s (a, b) = Some (UntypedCap deva r bits f)\<rbrakk> \<Longrightarrow> is_subject aag a
 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 3. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 4. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>_. silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)\<rbrace>
 2. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 3. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 2. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> (silc_inv aag st and cte_wp_at is_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) and invs and pas_refined aag and (\<lambda>s. descendants_of (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) (cdt 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> (cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> (True \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x))) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) and invs 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>authorised_untyped_inv aag ui; (silc_inv aag st and invs and pas_refined aag and ct_active and valid_untyped_inv ui) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> (silc_inv aag st and cte_wp_at is_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) and invs and pas_refined aag and (\<lambda>s. descendants_of (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) (cdt 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> (cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> (True \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x))) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) and invs 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 (silc_inv aag st and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x\<in>untyped_range cp. is_subject aag x)) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot)) 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>ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; silc_inv aag st s; 0 < word_of_nat (length x7); invs s; \<forall>x\<in>set (retype_addrs x4 x5 (length x7) x6). is_subject aag x; pas_refined aag s; \<forall>x\<in>{x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1}. is_subject aag x; ct_active s; x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set x7. is_subject aag (fst x); caps_of_state s (a, b) = Some (UntypedCap x8 (x4 && ~~ mask sz) sz idx); 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. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5\<rbrakk> \<Longrightarrow> (x2 \<longrightarrow> (\<forall>x\<in>{x4 && ~~ mask sz..(x4 && ~~ mask sz) + 2 ^ sz - 1}. is_subject aag x)) \<and> (\<forall>x\<in>{x4 && ~~ mask sz..(x4 && ~~ mask sz) + 2 ^ sz - 1}. is_subject aag x) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; silc_inv aag st s; 0 < word_of_nat (length x7); invs s; \<forall>x\<in>set (retype_addrs x4 x5 (length x7) x6). is_subject aag x; pas_refined aag s; \<forall>x\<in>{x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1}. is_subject aag x; ct_active s; x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set x7. is_subject aag (fst x); caps_of_state s (a, b) = Some (UntypedCap x8 (x4 && ~~ mask sz) sz idx); 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. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5; aag_cap_auth aag (pasObjectAbs aag (fst (a, b))) (UntypedCap x8 (x4 && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> (x2 \<longrightarrow> (\<forall>x\<in>{x4 && ~~ mask sz..(x4 && ~~ mask sz) + 2 ^ sz - 1}. is_subject aag x)) \<and> (\<forall>x\<in>{x4 && ~~ mask sz..(x4 && ~~ mask sz) + 2 ^ sz - 1}. is_subject aag x) proof (prove)
goal:
No subgoals!