theory Retype_AC

lemma reset_untyped_cap_pas_refined[wp]:
  "\<lbrace>pas_refined aag and invs and
                    (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s)
                    and K (is_subject aag (fst slot))\<rbrace>
   reset_untyped_cap slot
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (rule hoare_gen_asm) apply (clarsimp simp: reset_untyped_cap_def) apply (rule hoare_pre) apply (wps | wp set_cap_pas_refined_not_transferable | simp add: unless_def)+ apply (rule valid_validE) apply (rule_tac P="is_untyped_cap cap \<and> pas_cap_cur_auth aag cap" in hoare_gen_asm) apply (rule_tac Q="\<lambda>_. cte_wp_at (\<lambda> c. \<not> is_transferable (Some c)) slot and pas_refined aag and
                            pspace_aligned and valid_vspace_objs and valid_arch_state"
                  in hoare_strengthen_post) apply (rule validE_valid, rule mapME_x_inv_wp) apply (rule hoare_pre) apply (wps
             | wp preemption_point_inv' set_cap_pas_refined_not_transferable set_cap_sets_direct
             | simp)+ apply (fastforce simp: is_cap_simps aag_cap_auth_UntypedCap_idx_dev bits_of_def) apply blast apply (wps | wp hoare_vcg_const_imp_lift get_cap_wp delete_objects_pas_refined hoare_drop_imp
                    delete_objects_valid_vspace_objs delete_objects_valid_arch_state
               | simp)+ apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def) apply (frule cte_map_not_null_outside'[rotated]) apply (fastforce simp: cte_wp_at_caps_of_state)+ apply (cases slot) apply (auto elim: caps_pas_cap_cur_auth_UntypedCap_idx_dev) apply (fastforce simp: bits_of_def is_cap_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s) and K (is_subject aag (fst slot))\<rbrace> reset_untyped_cap slot \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s)\<rbrace> reset_untyped_cap slot \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s)\<rbrace> doE cap <- liftE (get_cap slot);
if free_index_of cap = 0 then returnOk () else doE y <- liftE (delete_objects (obj_ref_of cap) (bits_of cap));
if is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits then liftE (do y <- unless (is_device_untyped_cap cap) (do_machine_op (clearMemory (obj_ref_of cap) (2 ^ bits_of cap)));
set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) slot
od) else mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)]))
odE
odE \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> doE cap <- liftE (get_cap slot);
if free_index_of cap = 0 then returnOk () else doE y <- liftE (delete_objects (obj_ref_of cap) (bits_of cap));
if is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits then liftE (do y <- unless (is_device_untyped_cap cap) (do_machine_op (clearMemory (obj_ref_of cap) (2 ^ bits_of cap)));
set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) slot
od) else mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)]))
odE
odE \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. \<lbrakk>is_subject aag (fst slot); (pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s)) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap ()\<rbrace> mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)])) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s else (\<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> ?R15 cap y s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> pas_refined aag s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s)) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap ()\<rbrace> mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)])) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s else (\<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> ?R15 cap y s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> pas_refined aag s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s)) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; is_untyped_cap cap \<and> pas_cap_cur_auth aag cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'41 cap ()\<rbrace> mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)])) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s else (\<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (?P'41 cap y and K (is_untyped_cap cap \<and> pas_cap_cur_auth aag cap)) s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> pas_refined aag s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s)) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>cap. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; is_untyped_cap cap \<and> pas_cap_cur_auth aag cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'41 cap ()\<rbrace> mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)])) \<lbrace>\<lambda>_. cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
 2. \<And>cap rv s. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; is_untyped_cap cap \<and> pas_cap_cur_auth aag cap; (cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s else (\<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (?P'41 cap y and K (is_untyped_cap cap \<and> pas_cap_cur_auth aag cap)) s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 4. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> pas_refined aag s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 5. \<And>s. \<lbrakk>is_subject aag (fst slot); (pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s)) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>cap x. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; is_untyped_cap cap \<and> pas_cap_cur_auth aag cap\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of cap) (bits_of cap) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>, \<lbrace>\<lambda>_. cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
 2. \<And>cap rv s. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; is_untyped_cap cap \<and> pas_cap_cur_auth aag cap; (cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s else (\<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (is_untyped_cap cap \<and> pas_cap_cur_auth aag cap)) s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 4. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> pas_refined aag s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 5. \<And>s. \<lbrakk>is_subject aag (fst slot); (pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s)) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>cap x. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; is_untyped_cap cap \<and> pas_cap_cur_auth aag cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 cap x\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of cap) (bits_of cap) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>, \<lbrace>\<lambda>_. cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
 2. \<And>cap x s. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; is_untyped_cap cap \<and> pas_cap_cur_auth aag cap; (cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s\<rbrakk> \<Longrightarrow> ?Q48 cap x s
 3. \<And>cap rv s. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; is_untyped_cap cap \<and> pas_cap_cur_auth aag cap; (cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s else (\<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (is_untyped_cap cap \<and> pas_cap_cur_auth aag cap)) s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 5. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> pas_refined aag s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 6. \<And>s. \<lbrakk>is_subject aag (fst slot); (pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s)) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>cap x s. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; is_untyped_cap cap \<and> pas_cap_cur_auth aag cap; cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag (UntypedCap False (obj_ref_of cap) (bits_of cap) (x * 2 ^ resetChunkBits))
 2. \<And>cap rv s. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; is_untyped_cap cap \<and> pas_cap_cur_auth aag cap; (cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s else (\<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (is_untyped_cap cap \<and> pas_cap_cur_auth aag cap)) s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 4. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> pas_refined aag s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 5. \<And>s. \<lbrakk>is_subject aag (fst slot); (pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s)) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>cap rv s. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; is_untyped_cap cap \<and> pas_cap_cur_auth aag cap; (cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s else (\<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (is_untyped_cap cap \<and> pas_cap_cur_auth aag cap)) s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> pas_refined aag s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s)) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (3 subgoals):
 1. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s else (\<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) slot s \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) slot and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (is_untyped_cap cap \<and> pas_cap_cur_auth aag cap)) s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> pas_refined aag s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag (fst slot); (pas_refined aag and invs and (\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s)) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); pas_refined aag s \<and> invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> 0 < free_index_of cap \<longrightarrow> (is_device_untyped_cap cap \<longrightarrow> pspace_aligned s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (a, b) s \<and> untyped_range c = {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1}) (a, b) s) \<and> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) slot s \<and> (obj_ref_of cap \<le> fst slot \<longrightarrow> \<not> fst slot \<le> obj_ref_of cap + 2 ^ bits_of cap - 1) \<and> pas_cap_cur_auth aag (UntypedCap True (obj_ref_of cap) (bits_of cap) 0)) \<and> (bits_of cap < resetChunkBits \<longrightarrow> pspace_aligned s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (a, b) s \<and> untyped_range c = {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1}) (a, b) s) \<and> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) slot s \<and> (obj_ref_of cap \<le> fst slot \<longrightarrow> \<not> fst slot \<le> obj_ref_of cap + 2 ^ bits_of cap - 1) \<and> pas_cap_cur_auth aag (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits \<longrightarrow> cte_wp_at (\<lambda>a. \<not> is_transferable_cap a) slot s \<and> (obj_ref_of cap \<le> fst slot \<longrightarrow> \<not> fst slot \<le> obj_ref_of cap + 2 ^ bits_of cap - 1) \<and> pspace_aligned s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (a, b) s \<and> untyped_range c = {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1}) (a, b) s) \<and> is_untyped_cap cap \<and> pas_cap_cur_auth aag cap) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); pas_refined aag s; invs s; descendants_range (UntypedCap dev r bits f) slot s; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> pspace_aligned s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}) \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pas_cap_cur_auth aag (UntypedCap True r bits 0)) \<and> (bits < resetChunkBits \<longrightarrow> pspace_aligned s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}) \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pas_cap_cur_auth aag (UntypedCap dev r bits 0)) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pspace_aligned s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}) \<and> pas_cap_cur_auth aag (UntypedCap False r bits f)) proof (prove)
goal (6 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); pas_refined aag s; invs s; descendants_range (UntypedCap dev r bits f) slot s; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 2. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); pas_refined aag s; invs s; descendants_range (UntypedCap dev r bits f) slot s; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> if_unsafe_then_cap s
 3. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); pas_refined aag s; invs s; descendants_range (UntypedCap dev r bits f) slot s; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> valid_global_refs s
 4. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); pas_refined aag s; invs s; descendants_range (UntypedCap dev r bits f) slot s; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) (?p262 s dev r bits f) s
 5. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); pas_refined aag s; invs s; descendants_range (UntypedCap dev r bits f) slot s; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (UntypedCap dev r bits f)) slot s
 6. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); pas_refined aag s; invs s; descendants_range (UntypedCap dev r bits f) slot s; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); fst (?p262 s dev r bits f) \<notin> untyped_range (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> pspace_aligned s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}) \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pas_cap_cur_auth aag (UntypedCap True r bits 0)) \<and> (bits < resetChunkBits \<longrightarrow> pspace_aligned s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}) \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pas_cap_cur_auth aag (UntypedCap dev r bits 0)) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pspace_aligned s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}) \<and> pas_cap_cur_auth aag (UntypedCap False r bits f)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); pas_refined aag s; invs s; descendants_range (UntypedCap dev r bits f) slot s; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); fst slot \<notin> untyped_range (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> pspace_aligned s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}) \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pas_cap_cur_auth aag (UntypedCap True r bits 0)) \<and> (bits < resetChunkBits \<longrightarrow> pspace_aligned s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}) \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pas_cap_cur_auth aag (UntypedCap dev r bits 0)) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pspace_aligned s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}) \<and> pas_cap_cur_auth aag (UntypedCap False r bits f)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f a b. \<lbrakk>is_subject aag (fst slot); pas_refined aag s; invs s; descendants_range (UntypedCap dev r bits f) slot s; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); fst slot \<notin> untyped_range (UntypedCap dev r bits f); slot = (a, b)\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> pspace_aligned s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}) \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pas_cap_cur_auth aag (UntypedCap True r bits 0)) \<and> (bits < resetChunkBits \<longrightarrow> pspace_aligned s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}) \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pas_cap_cur_auth aag (UntypedCap dev r bits 0)) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pspace_aligned s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}) \<and> pas_cap_cur_auth aag (UntypedCap False r bits f)) proof (prove)
goal (6 subgoals):
 1. \<And>s dev r bits f a b. \<lbrakk>is_subject aag a; pas_refined aag s; invs s; descendants_range (UntypedCap True r bits f) (a, b) s; caps_of_state s (a, b) = Some (UntypedCap True r bits f); 0 < free_index_of (UntypedCap True r bits f); slot = (a, b); \<not> r \<le> a; dev\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}
 2. \<And>s dev r bits f a b. \<lbrakk>is_subject aag a; pas_refined aag s; invs s; descendants_range (UntypedCap dev r bits f) (a, b) s; caps_of_state s (a, b) = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); slot = (a, b); \<not> r \<le> a; bits < resetChunkBits\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}
 3. \<And>s dev r bits f a b. \<lbrakk>is_subject aag a; pas_refined aag s; invs s; descendants_range (UntypedCap False r bits f) (a, b) s; caps_of_state s (a, b) = Some (UntypedCap False r bits f); 0 < free_index_of (UntypedCap False r bits f); slot = (a, b); \<not> r \<le> a; \<not> dev; \<not> bits < resetChunkBits\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}
 4. \<And>s dev r bits f a b. \<lbrakk>is_subject aag a; pas_refined aag s; invs s; descendants_range (UntypedCap True r bits f) (a, b) s; caps_of_state s (a, b) = Some (UntypedCap True r bits f); 0 < free_index_of (UntypedCap True r bits f); slot = (a, b); \<not> a \<le> r + 2 ^ bits - 1; dev\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}
 5. \<And>s dev r bits f a b. \<lbrakk>is_subject aag a; pas_refined aag s; invs s; descendants_range (UntypedCap dev r bits f) (a, b) s; caps_of_state s (a, b) = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); slot = (a, b); \<not> a \<le> r + 2 ^ bits - 1; bits < resetChunkBits\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1}
 6. \<And>s dev r bits f a b. \<lbrakk>is_subject aag a; pas_refined aag s; invs s; descendants_range (UntypedCap False r bits f) (a, b) s; caps_of_state s (a, b) = Some (UntypedCap False r bits f); 0 < free_index_of (UntypedCap False r bits f); slot = (a, b); \<not> a \<le> r + 2 ^ bits - 1; \<not> dev; \<not> bits < resetChunkBits\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> descendants_range cap (a, b) s \<and> untyped_range cap = {r..r + 2 ^ bits - 1} proof (prove)
goal:
No subgoals!