theory ArchRetype_IF

lemma reset_untyped_cap_globals_equiv:
  "\<lbrace>globals_equiv st and invs and cte_wp_at is_untyped_cap slot
                     and ct_active and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>
   reset_untyped_cap slot
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (simp add: reset_untyped_cap_def cong: if_cong) apply (rule hoare_pre) apply (wp set_cap_globals_equiv dmo_clearMemory_globals_equiv
             preemption_point_inv | simp add: unless_def)+ apply (rule valid_validE) apply (rule_tac P="cap_aligned cap \<and> is_untyped_cap cap" in hoare_gen_asm) apply (rule_tac Q="\<lambda>_ s. valid_global_objs s \<and> valid_arch_state s \<and> globals_equiv st s"
                  in hoare_strengthen_post) apply (rule validE_valid, rule mapME_x_wp') apply (rule hoare_pre) apply (wp set_cap_globals_equiv dmo_clearMemory_globals_equiv
                 preemption_point_inv | simp add: if_apply_def2)+ apply (clarsimp simp: is_cap_simps ptr_range_def[symmetric]
                          cap_aligned_def bits_of_def
                          free_index_of_def) apply (clarsimp simp: Kernel_Config.resetChunkBits_def) apply (strengthen invs_valid_global_objs invs_arch_state) apply (wp delete_objects_invs_ex hoare_vcg_const_imp_lift get_cap_wp)+ apply (clarsimp simp: cte_wp_at_caps_of_state descendants_range_def2 is_cap_simps bits_of_def
             split del: if_split) apply (frule caps_of_state_valid_cap, clarsimp+) apply (clarsimp simp: valid_cap_simps cap_aligned_def untyped_min_bits_def) apply (frule valid_global_refsD2, clarsimp+) apply (clarsimp simp: ptr_range_def[symmetric] global_refs_def) apply (strengthen empty_descendants_range_in) apply (cases slot) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and invs and cte_wp_at is_untyped_cap slot and ct_active and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> reset_untyped_cap slot \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and invs and cte_wp_at is_untyped_cap slot and ct_active and (\<lambda>s. descendants_of slot (cdt 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>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<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>_. globals_equiv st\<rbrace>
 2. \<And>s. (globals_equiv st and invs and cte_wp_at is_untyped_cap slot and ct_active and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrakk>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>_. globals_equiv st\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>cap. free_index_of cap \<noteq> 0 \<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. globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s else (\<lambda>s. globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> ?R15 cap y s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> globals_equiv st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>s. (globals_equiv st and invs and cte_wp_at is_untyped_cap slot and ct_active and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrakk>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>_. globals_equiv st\<rbrace>
 2. \<And>cap. free_index_of cap \<noteq> 0 \<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. globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s else (\<lambda>s. globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> ?R15 cap y s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> globals_equiv st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>s. (globals_equiv st and invs and cte_wp_at is_untyped_cap slot and ct_active and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrakk>0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; cap_aligned cap \<and> is_untyped_cap cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'32 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>_. globals_equiv st\<rbrace>
 2. \<And>cap. free_index_of cap \<noteq> 0 \<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. globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s else (\<lambda>s. globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (?P'32 cap y and K (cap_aligned cap \<and> is_untyped_cap cap)) s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> globals_equiv st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>s. (globals_equiv st and invs and cte_wp_at is_untyped_cap slot and ct_active and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>cap. \<lbrakk>0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; cap_aligned cap \<and> is_untyped_cap cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'32 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>_ s. valid_global_objs s \<and> valid_arch_state s \<and> globals_equiv st s\<rbrace>
 2. \<And>cap rv s. \<lbrakk>0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; cap_aligned cap \<and> is_untyped_cap cap; valid_global_objs s \<and> valid_arch_state s \<and> globals_equiv st s\<rbrakk> \<Longrightarrow> globals_equiv st s
 3. \<And>cap. free_index_of cap \<noteq> 0 \<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. globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s else (\<lambda>s. globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (?P'32 cap y and K (cap_aligned cap \<and> is_untyped_cap cap)) s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> globals_equiv st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>s. (globals_equiv st and invs and cte_wp_at is_untyped_cap slot and ct_active and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>cap x. \<lbrakk>0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; cap_aligned cap \<and> is_untyped_cap cap; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. valid_global_objs a \<and> valid_arch_state a \<and> globals_equiv st a\<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>_ a. valid_global_objs a \<and> valid_arch_state a \<and> globals_equiv st a\<rbrace>, \<lbrace>\<lambda>_ a. valid_global_objs a \<and> valid_arch_state a \<and> globals_equiv st a\<rbrace>
 2. \<And>cap rv s. \<lbrakk>0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; cap_aligned cap \<and> is_untyped_cap cap; valid_global_objs s \<and> valid_arch_state s \<and> globals_equiv st s\<rbrakk> \<Longrightarrow> globals_equiv st s
 3. \<And>cap. free_index_of cap \<noteq> 0 \<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. globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s else (\<lambda>s. globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> ((\<lambda>a. valid_global_objs a \<and> valid_arch_state a \<and> globals_equiv st a) and K (cap_aligned cap \<and> is_untyped_cap cap)) s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> globals_equiv st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>s. (globals_equiv st and invs and cte_wp_at is_untyped_cap slot and ct_active and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>cap x. \<lbrakk>0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; cap_aligned cap \<and> is_untyped_cap cap; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>?Q39 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>_ a. valid_global_objs a \<and> valid_arch_state a \<and> globals_equiv st a\<rbrace>, \<lbrace>\<lambda>_ a. valid_global_objs a \<and> valid_arch_state a \<and> globals_equiv st a\<rbrace>
 2. \<And>cap x s. \<lbrakk>0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; cap_aligned cap \<and> is_untyped_cap cap; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)])); valid_global_objs s \<and> valid_arch_state s \<and> globals_equiv st s\<rbrakk> \<Longrightarrow> ?Q39 cap x s
 3. \<And>cap rv s. \<lbrakk>0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; cap_aligned cap \<and> is_untyped_cap cap; valid_global_objs s \<and> valid_arch_state s \<and> globals_equiv st s\<rbrakk> \<Longrightarrow> globals_equiv st s
 4. \<And>cap. free_index_of cap \<noteq> 0 \<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. globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s else (\<lambda>s. globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> ((\<lambda>a. valid_global_objs a \<and> valid_arch_state a \<and> globals_equiv st a) and K (cap_aligned cap \<and> is_untyped_cap cap)) s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> globals_equiv st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<And>s. (globals_equiv st and invs and cte_wp_at is_untyped_cap slot and ct_active and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (3 subgoals):
 1. \<And>cap. 0 < free_index_of cap \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> delete_objects (obj_ref_of cap) (bits_of cap) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<longrightarrow> globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s) \<and> (bits_of cap < resetChunkBits \<longrightarrow> globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits \<longrightarrow> valid_global_objs s \<and> valid_arch_state s \<and> globals_equiv st s \<and> cap_aligned cap \<and> is_untyped_cap cap)\<rbrace>
 2. \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> globals_equiv st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>s. (globals_equiv st and invs and cte_wp_at is_untyped_cap slot and ct_active and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (3 subgoals):
 1. \<And>cap. 0 < (case cap of UntypedCap x xa xb free_index \<Rightarrow> free_index) \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> delete_objects (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<longrightarrow> globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s) \<and> ((case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < resetChunkBits \<longrightarrow> globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < resetChunkBits \<longrightarrow> valid_global_objs s \<and> valid_arch_state s \<and> globals_equiv st s \<and> is_aligned (obj_ref_of cap) (cap_bits cap) \<and> cap_bits cap < word_bits \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f))\<rbrace>
 2. \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> globals_equiv st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>s. (globals_equiv st and invs and cte_wp_at is_untyped_cap slot and ct_active and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (3 subgoals):
 1. \<And>cap. 0 < (case cap of UntypedCap x xa xb free_index \<Rightarrow> free_index) \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> delete_objects (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<longrightarrow> globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s) \<and> ((case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < 8 \<longrightarrow> globals_equiv st s \<and> valid_global_objs s \<and> valid_arch_state s) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < 8 \<longrightarrow> valid_global_objs s \<and> valid_arch_state s \<and> globals_equiv st s \<and> is_aligned (obj_ref_of cap) (cap_bits cap) \<and> cap_bits cap < word_bits \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f))\<rbrace>
 2. \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> globals_equiv st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>s. (globals_equiv st and invs and cte_wp_at is_untyped_cap slot and ct_active and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (3 subgoals):
 1. \<And>cap. 0 < (case cap of UntypedCap x xa xb free_index \<Rightarrow> free_index) \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> delete_objects (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) \<lbrace>\<lambda>r s. (is_device_untyped_cap cap \<longrightarrow> globals_equiv st s \<and> invs s \<and> invs s) \<and> ((case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < 8 \<longrightarrow> globals_equiv st s \<and> invs s \<and> invs s) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < 8 \<longrightarrow> invs s \<and> invs s \<and> globals_equiv st s \<and> is_aligned (obj_ref_of cap) (cap_bits cap) \<and> cap_bits cap < word_bits \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f))\<rbrace>
 2. \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> globals_equiv st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>s. (globals_equiv st and invs and cte_wp_at is_untyped_cap slot and ct_active and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (globals_equiv st and invs and cte_wp_at is_untyped_cap slot and ct_active and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (free_index_of cap = 0 \<longrightarrow> globals_equiv st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> (is_device_untyped_cap cap \<longrightarrow> (globals_equiv st and (\<lambda>s. is_aligned (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) \<and> 2 \<le> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) \<and> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < word_bits \<and> arm_global_pd (arch_state s) \<notin> ptr_range (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) \<and> idle_thread s \<notin> ptr_range (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits))) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) f) slot s)) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) f) slot s)) s) \<and> ((case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < 8 \<longrightarrow> (globals_equiv st and (\<lambda>s. is_aligned (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) \<and> 2 \<le> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) \<and> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < word_bits \<and> arm_global_pd (arch_state s) \<notin> ptr_range (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) \<and> idle_thread s \<notin> ptr_range (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits))) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) f) slot s)) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) f) slot s)) s) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < 8 \<longrightarrow> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) f) slot s)) s \<and> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) f) slot s)) s \<and> (globals_equiv st and (\<lambda>s. is_aligned (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) \<and> 2 \<le> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) \<and> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < word_bits \<and> arm_global_pd (arch_state s) \<notin> ptr_range (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) \<and> idle_thread s \<notin> ptr_range (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits))) s \<and> is_aligned (obj_ref_of cap) (cap_bits cap) \<and> cap_bits cap < word_bits \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f))) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>globals_equiv st s; invs s; ct_active s; descendants_of slot (cdt 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> is_aligned r bits \<and> 2 \<le> bits \<and> bits < word_bits \<and> arm_global_pd (arch_state s) \<notin> ptr_range r bits \<and> idle_thread s \<notin> ptr_range r bits \<and> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in {r..r + 2 ^ bits - 1} (a, b) s)) \<and> (bits < 8 \<longrightarrow> is_aligned r bits \<and> 2 \<le> bits \<and> bits < word_bits \<and> arm_global_pd (arch_state s) \<notin> ptr_range r bits \<and> idle_thread s \<notin> ptr_range r bits \<and> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in {r..r + 2 ^ bits - 1} (a, b) s)) \<and> (\<not> dev \<and> \<not> bits < 8 \<longrightarrow> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in {r..r + 2 ^ bits - 1} (a, b) s) \<and> is_aligned r bits \<and> bits < word_bits \<and> arm_global_pd (arch_state s) \<notin> ptr_range r bits \<and> idle_thread s \<notin> ptr_range r bits \<and> is_aligned r bits \<and> bits < word_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>globals_equiv st s; invs s; ct_active s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); s \<turnstile> UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> is_aligned r bits \<and> 2 \<le> bits \<and> bits < word_bits \<and> arm_global_pd (arch_state s) \<notin> ptr_range r bits \<and> idle_thread s \<notin> ptr_range r bits \<and> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in {r..r + 2 ^ bits - 1} (a, b) s)) \<and> (bits < 8 \<longrightarrow> is_aligned r bits \<and> 2 \<le> bits \<and> bits < word_bits \<and> arm_global_pd (arch_state s) \<notin> ptr_range r bits \<and> idle_thread s \<notin> ptr_range r bits \<and> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in {r..r + 2 ^ bits - 1} (a, b) s)) \<and> (\<not> dev \<and> \<not> bits < 8 \<longrightarrow> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in {r..r + 2 ^ bits - 1} (a, b) s) \<and> is_aligned r bits \<and> bits < word_bits \<and> arm_global_pd (arch_state s) \<notin> ptr_range r bits \<and> idle_thread s \<notin> ptr_range r bits \<and> is_aligned r bits \<and> bits < word_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>globals_equiv st s; invs s; ct_active s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; 4 \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> arm_global_pd (arch_state s) \<notin> ptr_range r bits \<and> idle_thread s \<notin> ptr_range r bits \<and> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in {r..r + 2 ^ bits - 1} (a, b) s)) \<and> (bits < 8 \<longrightarrow> arm_global_pd (arch_state s) \<notin> ptr_range r bits \<and> idle_thread s \<notin> ptr_range r bits \<and> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in {r..r + 2 ^ bits - 1} (a, b) s)) \<and> (\<not> dev \<and> \<not> bits < 8 \<longrightarrow> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in {r..r + 2 ^ bits - 1} (a, b) s) \<and> arm_global_pd (arch_state s) \<notin> ptr_range r bits \<and> idle_thread s \<notin> ptr_range r bits) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>globals_equiv st s; invs s; ct_active s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; 4 \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; global_refs s \<inter> {r..r + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> arm_global_pd (arch_state s) \<notin> ptr_range r bits \<and> idle_thread s \<notin> ptr_range r bits \<and> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in {r..r + 2 ^ bits - 1} (a, b) s)) \<and> (bits < 8 \<longrightarrow> arm_global_pd (arch_state s) \<notin> ptr_range r bits \<and> idle_thread s \<notin> ptr_range r bits \<and> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in {r..r + 2 ^ bits - 1} (a, b) s)) \<and> (\<not> dev \<and> \<not> bits < 8 \<longrightarrow> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in {r..r + 2 ^ bits - 1} (a, b) s) \<and> arm_global_pd (arch_state s) \<notin> ptr_range r bits \<and> idle_thread s \<notin> ptr_range r bits) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>globals_equiv st s; invs s; ct_active s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; 4 \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; idle_thread s \<notin> ptr_range r bits; arm_global_pd (arch_state s) \<notin> ptr_range r bits; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> ptr_range r bits = {}\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in (ptr_range r bits) (a, b) s)) \<and> (bits < 8 \<longrightarrow> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in (ptr_range r bits) (a, b) s)) \<and> (\<not> dev \<and> \<not> bits < 8 \<longrightarrow> (\<exists>a b. (\<exists>dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f)) \<and> descendants_range_in (ptr_range r bits) (a, b) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>globals_equiv st s; invs s; ct_active s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; 4 \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; idle_thread s \<notin> ptr_range r bits; arm_global_pd (arch_state s) \<notin> ptr_range r bits; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> ptr_range r bits = {}\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> (\<exists>x xa. (\<exists>dev f. caps_of_state s (x, xa) = Some (UntypedCap dev r bits f)) \<and> descendants_of (x, xa) (cdt s) = {})) \<and> (bits < 8 \<longrightarrow> (\<exists>x xa. (\<exists>dev f. caps_of_state s (x, xa) = Some (UntypedCap dev r bits f)) \<and> descendants_of (x, xa) (cdt s) = {})) \<and> (\<not> dev \<and> \<not> bits < 8 \<longrightarrow> (\<exists>x xa. (\<exists>dev f. caps_of_state s (x, xa) = Some (UntypedCap dev r bits f)) \<and> descendants_of (x, xa) (cdt s) = {})) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f a b. \<lbrakk>globals_equiv st s; invs s; ct_active s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; 4 \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; idle_thread s \<notin> ptr_range r bits; arm_global_pd (arch_state s) \<notin> ptr_range r bits; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> ptr_range r bits = {}; slot = (a, b)\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> (\<exists>x xa. (\<exists>dev f. caps_of_state s (x, xa) = Some (UntypedCap dev r bits f)) \<and> descendants_of (x, xa) (cdt s) = {})) \<and> (bits < 8 \<longrightarrow> (\<exists>x xa. (\<exists>dev f. caps_of_state s (x, xa) = Some (UntypedCap dev r bits f)) \<and> descendants_of (x, xa) (cdt s) = {})) \<and> (\<not> dev \<and> \<not> bits < 8 \<longrightarrow> (\<exists>x xa. (\<exists>dev f. caps_of_state s (x, xa) = Some (UntypedCap dev r bits f)) \<and> descendants_of (x, xa) (cdt s) = {})) proof (prove)
goal:
No subgoals!