theory ArchRetype_IF

lemma reset_untyped_cap_reads_respects_g:
 "reads_equiv_valid_g_inv (affects_equiv aag (l :: 'a subject_label)) aag
    (\<lambda>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and>
         is_subject aag (fst slot) \<and> (descendants_of slot (cdt s) = {}))
    (reset_untyped_cap slot)" apply (simp add: reset_untyped_cap_def cong: if_cong) apply (rule equiv_valid_guard_imp) apply (wp set_cap_reads_respects_g dmo_clearMemory_reads_respects_g
          | simp add: unless_def when_def split del: if_split)+ apply (rule_tac I="invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv
                                                 \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv)
                                                 \<and> free_index_of rv \<le> 2 ^ (bits_of rv)
                                                 \<and> is_subject aag (fst slot)) slot
                               and pspace_no_overlap (untyped_range rv)
                               and only_timer_irq_inv irq st
                               and (\<lambda>s. descendants_of slot (cdt s) = {})" in mapME_x_ev) apply (rule equiv_valid_guard_imp) apply wp apply (rule reads_respects_g_from_inv) apply (rule preemption_point_reads_respects[where irq=irq and st=st]) apply ((wp preemption_point_inv set_cap_reads_respects_g set_untyped_cap_invs_simple
                       only_timer_irq_inv_pres[where Q=\<top>, OF _ set_cap_domain_sep_inv]
                       dmo_clearMemory_reads_respects_g
                     | simp)+) apply (strengthen empty_descendants_range_in) apply (wp only_timer_irq_inv_pres[where P=\<top> and Q=\<top>] no_irq_clearMemory
                | simp | wp (once) dmo_wp)+ apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def) apply (frule(1) caps_of_state_valid) apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps
                              free_index_of_def invs_valid_global_objs) apply (simp add: aligned_add_aligned is_aligned_shiftl) apply (clarsimp simp: Kernel_Config.resetChunkBits_def) apply (rule hoare_pre) apply (wp preemption_point_inv' set_untyped_cap_invs_simple set_cap_cte_wp_at
                  set_cap_no_overlap only_timer_irq_inv_pres[where Q=\<top>, OF _ set_cap_domain_sep_inv]
               | simp)+ apply (strengthen empty_descendants_range_in) apply (wp only_timer_irq_inv_pres[where P=\<top> and Q=\<top>] no_irq_clearMemory
                | simp | wp (once) dmo_wp)+ apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def) apply (frule(1) caps_of_state_valid) apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps free_index_of_def) apply (wp | simp)+ apply (wp delete_objects_reads_respects_g) apply (simp add: if_apply_def2) apply (strengthen invs_valid_global_objs) apply (wp add: delete_objects_invs_ex hoare_vcg_const_imp_lift
                     delete_objects_pspace_no_overlap_again
                     delete_objects_valid_arch_state
                     only_timer_irq_inv_pres[where P=\<top> and Q=\<top>]
                del: Untyped_AI.delete_objects_pspace_no_overlap
             | simp)+ apply (rule get_cap_reads_respects_g) apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def) apply (frule(1) caps_of_state_valid) apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps
                        free_index_of_def invs_valid_global_objs) apply (frule valid_global_refsD2, clarsimp+) apply (clarsimp simp: ptr_range_def[symmetric] global_refs_def descendants_range_def2) apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], clarsimp+) apply (strengthen refl[where t=True] refl ex_tupleI[where t=slot] empty_descendants_range_in
         | clarsimp)+ apply (drule ex_cte_cap_protects[OF _ _ _ _ order_refl], erule caps_of_state_cteD) apply (clarsimp simp: descendants_range_def2 empty_descendants_range_in) apply clarsimp+ apply (fastforce simp: untyped_min_bits_def ptr_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {}) (reset_untyped_cap slot) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {}) (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) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?Q6 (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)
 2. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>rv. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?Q14 rv ()) (mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)])))
 2. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 3. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> ?Q14 rv rva s)\<rbrace>, -
 4. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 5. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 6. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (7 subgoals):
 1. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) (doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE)
 2. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>, -
 3. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 4. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 5. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 6. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 7. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (8 subgoals):
 1. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?Q38 rv x) (doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE)
 2. \<And>rv x s. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)])); (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> ?Q38 rv x s
 3. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>, -
 4. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 5. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 6. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 7. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 8. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (12 subgoals):
 1. \<And>rv x rva rvb. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?Q43 rv x rva rvb) preemption_point
 2. \<And>rv x rva. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'43 rv x rva) (liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot))
 3. \<And>rv x rva. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>?P''43 rv x rva\<rbrace> liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot) \<lbrace>?Q43 rv x rva\<rbrace>, -
 4. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'42 rv x) (liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits))))
 5. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>?P''42 rv x\<rbrace> liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits))) \<lbrace>\<lambda>rva s. ?P'43 rv x rva s \<and> ?P''43 rv x rva s\<rbrace>, -
 6. \<And>rv x s. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)])); (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> ?P'42 rv x s \<and> ?P''42 rv x s
 7. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>, -
 8. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 9. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 10. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv x rva rvb. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q43 rv x rva rvb) preemption_point
 2. \<And>rv x rva rvb st. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>globals_equiv st\<rbrace> preemption_point \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>rv x rva. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'43 rv x rva) (liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot))
 4. \<And>rv x rva. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>?P''43 rv x rva\<rbrace> liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot) \<lbrace>?Q43 rv x rva\<rbrace>, -
 5. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'42 rv x) (liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits))))
 6. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>?P''42 rv x\<rbrace> liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits))) \<lbrace>\<lambda>rva s. ?P'43 rv x rva s \<and> ?P''43 rv x rva s\<rbrace>, -
 7. \<And>rv x s. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)])); (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> ?P'42 rv x s \<and> ?P''42 rv x s
 8. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>, -
 9. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 10. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv x rva rvb st. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>globals_equiv st\<rbrace> preemption_point \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>rv x rva. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'43 rv x rva) (liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot))
 3. \<And>rv x rva. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>?P''43 rv x rva\<rbrace> liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot) \<lbrace>\<lambda>rvb. invs and only_timer_irq_inv irq st\<rbrace>, -
 4. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'42 rv x) (liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits))))
 5. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>?P''42 rv x\<rbrace> liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits))) \<lbrace>\<lambda>rva s. ?P'43 rv x rva s \<and> ?P''43 rv x rva s\<rbrace>, -
 6. \<And>rv x s. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)])); (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> ?P'42 rv x s \<and> ?P''42 rv x s
 7. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>, -
 8. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 9. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 10. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
A total of 12 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>rv x. \<lbrakk>\<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x < 2 ^ (bits_of rv - resetChunkBits) \<and> x * 2 ^ resetChunkBits < free_index_of rv\<rbrakk> \<Longrightarrow> \<lbrace>?P'86 rv x\<rbrace> do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)) \<lbrace>\<lambda>rva s. descendants_range_in {obj_ref_of rv..obj_ref_of rv + 2 ^ bits_of rv - 1} slot s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of rv) (bits_of rv)) s \<and> invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = bits_of rv \<and> obj_ref_of c = obj_ref_of rv \<and> \<not> cap_is_device c) slot s \<and> x * 2 ^ resetChunkBits \<le> 2 ^ bits_of rv \<and> only_timer_irq_inv irq st s\<rbrace>
 2. \<And>rv x s. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)])); (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> True \<and> valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s \<and> ?P'86 rv x s
 3. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>, -
 4. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 5. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 6. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 7. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 8. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (8 subgoals):
 1. \<And>rv x. \<lbrakk>\<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x < 2 ^ (bits_of rv - resetChunkBits) \<and> x * 2 ^ resetChunkBits < free_index_of rv\<rbrakk> \<Longrightarrow> \<lbrace>?P'86 rv x\<rbrace> do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)) \<lbrace>\<lambda>r s. descendants_of slot (cdt s) = {} \<and> pspace_no_overlap (up_aligned_area (obj_ref_of rv) (bits_of rv)) s \<and> invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = bits_of rv \<and> obj_ref_of c = obj_ref_of rv \<and> \<not> cap_is_device c) slot s \<and> x * 2 ^ resetChunkBits \<le> 2 ^ bits_of rv \<and> only_timer_irq_inv irq st s\<rbrace>
 2. \<And>rv x s. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)])); (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> True \<and> valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s \<and> ?P'86 rv x s
 3. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>, -
 4. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 5. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 6. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 7. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 8. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (7 subgoals):
 1. \<And>rv x s. \<lbrakk>\<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x < 2 ^ (bits_of rv - resetChunkBits) \<and> x * 2 ^ resetChunkBits < free_index_of rv; invs s \<and> cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot s \<and> pspace_no_overlap (untyped_range rv) s \<and> only_timer_irq_inv irq st s \<and> descendants_of slot (cdt s) = {}\<rbrakk> \<Longrightarrow> valid_global_objs s \<and> valid_arch_state s \<and> is_subject aag (fst slot) \<and> pspace_no_overlap (up_aligned_area (obj_ref_of rv) (bits_of rv)) s \<and> cte_wp_at (\<lambda>a. is_untyped_cap a \<and> cap_bits a = bits_of rv \<and> obj_ref_of a = obj_ref_of rv \<and> \<not> cap_is_device a) slot s \<and> x * 2 ^ resetChunkBits \<le> 2 ^ bits_of rv
 2. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>, -
 3. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 4. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 5. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 6. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 7. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (7 subgoals):
 1. \<And>x s dev r bits f idx. \<lbrakk>\<not> dev; \<not> bits < resetChunkBits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); invs s; pspace_no_overlap {r..r + 2 ^ bits - 1} s; caps_of_state s slot = Some (UntypedCap False r bits idx); only_timer_irq_inv irq st s; descendants_of slot (cdt s) = {}; free_index_of (UntypedCap False r bits f) \<le> 2 ^ bits; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> valid_global_objs s \<and> valid_arch_state s \<and> pspace_no_overlap (up_aligned_area r bits) s
 2. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>, -
 3. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 4. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 5. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 6. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 7. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (7 subgoals):
 1. \<And>x s dev r bits f idx. \<lbrakk>\<not> dev; \<not> bits < resetChunkBits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); invs s; pspace_no_overlap {r..r + 2 ^ bits - 1} s; caps_of_state s slot = Some (UntypedCap False r bits idx); only_timer_irq_inv irq st s; descendants_of slot (cdt s) = {}; free_index_of (UntypedCap False r bits f) \<le> 2 ^ bits; is_subject aag (fst slot); s \<turnstile> UntypedCap False r bits idx\<rbrakk> \<Longrightarrow> valid_global_objs s \<and> valid_arch_state s \<and> pspace_no_overlap (up_aligned_area r bits) s
 2. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>, -
 3. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 4. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 5. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 6. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 7. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (6 subgoals):
 1. \<And>rv x. \<lbrakk>0 < free_index_of rv; \<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of rv) [0..<2 ^ (bits_of rv - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>, -
 2. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 3. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 4. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 5. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 6. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (6 subgoals):
 1. \<And>rv x. \<lbrakk>\<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits; x < 2 ^ (bits_of rv - resetChunkBits) \<and> x * 2 ^ resetChunkBits < free_index_of rv\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>, -
 2. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 3. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 4. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 5. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 6. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (6 subgoals):
 1. \<And>rv x. \<lbrakk>\<not> is_device_untyped_cap rv; \<not> bits_of rv < 8; x < 2 ^ (bits_of rv - 8); x * 256 < free_index_of rv\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << 8)) 256));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 256)) slot);
preemption_point
odE \<lbrace>\<lambda>_. invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>, -
 2. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 3. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 4. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 5. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 6. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (7 subgoals):
 1. \<And>rv x. \<lbrakk>\<not> is_device_untyped_cap rv; \<not> bits_of rv < 8; x < 2 ^ (bits_of rv - 8); x * 256 < free_index_of rv\<rbrakk> \<Longrightarrow> \<lbrace>?P'154 rv x\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << 8)) 256));
y <- liftE (set_cap (UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 256)) slot);
preemption_point
odE \<lbrace>\<lambda>_. invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>, -
 2. \<And>rv x s. \<lbrakk>\<not> is_device_untyped_cap rv; \<not> bits_of rv < 8; x < 2 ^ (bits_of rv - 8); x * 256 < free_index_of rv; (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> ?P'154 rv x s
 3. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 4. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 5. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 6. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 7. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (7 subgoals):
 1. \<And>rv x. \<lbrakk>\<not> is_device_untyped_cap rv; \<not> bits_of rv < 8; x < 2 ^ (bits_of rv - 8); x * 256 < free_index_of rv\<rbrakk> \<Longrightarrow> \<lbrace>?P'214 rv x\<rbrace> do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << 8)) 256) \<lbrace>\<lambda>rva s. descendants_range_in {obj_ref_of rv..obj_ref_of rv + 2 ^ bits_of rv - 1} slot s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of rv) (bits_of rv)) s \<and> invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = bits_of rv \<and> obj_ref_of c = obj_ref_of rv \<and> \<not> cap_is_device c) slot s \<and> x * 256 \<le> 2 ^ bits_of rv \<and> is_untyped_cap rv \<and> (\<exists>idx. UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 256) = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot) \<and> cte_wp_at (\<lambda>_. True) slot s \<and> pspace_no_overlap (untyped_range rv) s \<and> only_timer_irq_inv irq st s \<and> descendants_of slot (cdt s) = {}\<rbrace>
 2. \<And>rv x s. \<lbrakk>\<not> is_device_untyped_cap rv; \<not> bits_of rv < 8; x < 2 ^ (bits_of rv - 8); x * 256 < free_index_of rv; (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> True \<and> True \<and> ?P'214 rv x s
 3. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 4. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 5. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 6. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 7. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (7 subgoals):
 1. \<And>rv x. \<lbrakk>\<not> is_device_untyped_cap rv; \<not> bits_of rv < 8; x < 2 ^ (bits_of rv - 8); x * 256 < free_index_of rv\<rbrakk> \<Longrightarrow> \<lbrace>?P'214 rv x\<rbrace> do_machine_op (clearMemory (obj_ref_of rv + (word_of_nat x << 8)) 256) \<lbrace>\<lambda>r s. descendants_of slot (cdt s) = {} \<and> pspace_no_overlap (up_aligned_area (obj_ref_of rv) (bits_of rv)) s \<and> invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = bits_of rv \<and> obj_ref_of c = obj_ref_of rv \<and> \<not> cap_is_device c) slot s \<and> x * 256 \<le> 2 ^ bits_of rv \<and> is_untyped_cap rv \<and> (\<exists>idx. UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 256) = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot) \<and> cte_wp_at (\<lambda>_. True) slot s \<and> pspace_no_overlap (untyped_range rv) s \<and> only_timer_irq_inv irq st s \<and> descendants_of slot (cdt s) = {}\<rbrace>
 2. \<And>rv x s. \<lbrakk>\<not> is_device_untyped_cap rv; \<not> bits_of rv < 8; x < 2 ^ (bits_of rv - 8); x * 256 < free_index_of rv; (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> True \<and> True \<and> ?P'214 rv x s
 3. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 4. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 5. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 6. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 7. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (6 subgoals):
 1. \<And>rv x s. \<lbrakk>\<not> is_device_untyped_cap rv; \<not> bits_of rv < 8; x < 2 ^ (bits_of rv - 8); x * 256 < free_index_of rv; invs s \<and> cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot s \<and> pspace_no_overlap (untyped_range rv) s \<and> only_timer_irq_inv irq st s \<and> descendants_of slot (cdt s) = {}\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area (obj_ref_of rv) (bits_of rv)) s \<and> cte_wp_at (\<lambda>a. is_untyped_cap a \<and> cap_bits a = bits_of rv \<and> obj_ref_of a = obj_ref_of rv \<and> \<not> cap_is_device a) slot s \<and> x * 256 \<le> 2 ^ bits_of rv \<and> is_untyped_cap rv \<and> (\<exists>idx. UntypedCap False (obj_ref_of rv) (bits_of rv) (x * 256) = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot) \<and> cte_wp_at (\<lambda>a. True) slot s
 2. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 3. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 4. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 5. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 6. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (6 subgoals):
 1. \<And>x s dev r bits f idx. \<lbrakk>\<not> dev; \<not> bits < 8; x < 2 ^ (bits - 8); x * 256 < free_index_of (UntypedCap False r bits f); invs s; pspace_no_overlap {r..r + 2 ^ bits - 1} s; caps_of_state s slot = Some (UntypedCap False r bits idx); only_timer_irq_inv irq st s; descendants_of slot (cdt s) = {}; free_index_of (UntypedCap False r bits f) \<le> 2 ^ bits; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area r bits) s
 2. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 3. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 4. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 5. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 6. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (6 subgoals):
 1. \<And>x s dev r bits f idx. \<lbrakk>\<not> dev; \<not> bits < 8; x < 2 ^ (bits - 8); x * 256 < free_index_of (UntypedCap False r bits f); invs s; pspace_no_overlap {r..r + 2 ^ bits - 1} s; caps_of_state s slot = Some (UntypedCap False r bits idx); only_timer_irq_inv irq st s; descendants_of slot (cdt s) = {}; free_index_of (UntypedCap False r bits f) \<le> 2 ^ bits; is_subject aag (fst slot); s \<turnstile> UntypedCap False r bits idx\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area r bits) s
 2. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 3. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 4. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 5. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 6. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (5 subgoals):
 1. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (liftE (delete_objects (obj_ref_of rv) (bits_of rv)))
 2. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 3. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 4. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 5. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (5 subgoals):
 1. \<And>rv. 0 < free_index_of rv \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'13 rv) (delete_objects (obj_ref_of rv) (bits_of rv))
 2. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 3. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 4. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> ?P'13 rv s \<and> ?P''13 rv s)\<rbrace>, -
 5. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (4 subgoals):
 1. \<And>rv. free_index_of rv \<noteq> 0 \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits \<longrightarrow> ((\<not> is_device_untyped_cap rv \<longrightarrow> True) \<and> (\<not> \<not> is_device_untyped_cap rv \<longrightarrow> True)) \<and> (if is_device_untyped_cap rv then \<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. valid_global_objs s \<and> valid_arch_state s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap rv \<or> bits_of rv < resetChunkBits) \<longrightarrow> (invs and cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot and pspace_no_overlap (untyped_range rv) and only_timer_irq_inv irq st and (\<lambda>s. descendants_of slot (cdt s) = {})) s)\<rbrace>, -
 2. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 3. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> (arm_global_pd (arch_state s) \<notin> ptr_range (obj_ref_of rv) (bits_of rv) \<and> idle_thread s \<notin> ptr_range (obj_ref_of rv) (bits_of rv) \<and> is_aligned (obj_ref_of rv) (bits_of rv) \<and> 2 \<le> bits_of rv \<and> bits_of rv < word_bits) \<and> ?P''13 rv s)\<rbrace>, -
 4. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (4 subgoals):
 1. \<And>rv. 0 < free_index_of rv \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>rva s. (is_device_untyped_cap rv \<longrightarrow> valid_global_objs s \<and> valid_arch_state s \<and> is_subject aag (fst slot)) \<and> (bits_of rv < resetChunkBits \<longrightarrow> valid_global_objs s \<and> valid_arch_state s \<and> is_subject aag (fst slot)) \<and> (\<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits \<longrightarrow> invs s \<and> cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot s \<and> pspace_no_overlap (untyped_range rv) s \<and> only_timer_irq_inv irq st s \<and> descendants_of slot (cdt s) = {})\<rbrace>, -
 2. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 3. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> (arm_global_pd (arch_state s) \<notin> ptr_range (obj_ref_of rv) (bits_of rv) \<and> idle_thread s \<notin> ptr_range (obj_ref_of rv) (bits_of rv) \<and> is_aligned (obj_ref_of rv) (bits_of rv) \<and> 2 \<le> bits_of rv \<and> bits_of rv < word_bits) \<and> ?P''13 rv s)\<rbrace>, -
 4. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (4 subgoals):
 1. \<And>rv. 0 < free_index_of rv \<Longrightarrow> \<lbrace>?P''13 rv\<rbrace> liftE (delete_objects (obj_ref_of rv) (bits_of rv)) \<lbrace>\<lambda>r s. (is_device_untyped_cap rv \<longrightarrow> invs s \<and> valid_arch_state s \<and> is_subject aag (fst slot)) \<and> (bits_of rv < resetChunkBits \<longrightarrow> invs s \<and> valid_arch_state s \<and> is_subject aag (fst slot)) \<and> (\<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits \<longrightarrow> invs s \<and> cte_wp_at (\<lambda>cp. is_untyped_cap rv \<and> (\<exists>idx. cp = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot s \<and> pspace_no_overlap (untyped_range rv) s \<and> only_timer_irq_inv irq st s \<and> descendants_of slot (cdt s) = {})\<rbrace>, -
 2. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (liftE (get_cap slot))
 3. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> (arm_global_pd (arch_state s) \<notin> ptr_range (obj_ref_of rv) (bits_of rv) \<and> idle_thread s \<notin> ptr_range (obj_ref_of rv) (bits_of rv) \<and> is_aligned (obj_ref_of rv) (bits_of rv) \<and> 2 \<le> bits_of rv \<and> bits_of rv < word_bits) \<and> ?P''13 rv s)\<rbrace>, -
 4. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (3 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'10 (get_cap slot)
 2. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> (arm_global_pd (arch_state s) \<notin> ptr_range (obj_ref_of rv) (bits_of rv) \<and> idle_thread s \<notin> ptr_range (obj_ref_of rv) (bits_of rv) \<and> is_aligned (obj_ref_of rv) (bits_of rv) \<and> 2 \<le> bits_of rv \<and> bits_of rv < word_bits) \<and> (is_device_untyped_cap rv \<longrightarrow> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of rv) (bits_of rv) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of rv) (bits_of rv) f) slot s)) s \<and> (invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {obj_ref_of rv..obj_ref_of rv + 2 ^ bits_of rv - 1}) ptr s)) \<and> is_subject aag (fst slot)) \<and> (bits_of rv < resetChunkBits \<longrightarrow> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of rv) (bits_of rv) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of rv) (bits_of rv) f) slot s)) s \<and> (invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {obj_ref_of rv..obj_ref_of rv + 2 ^ bits_of rv - 1}) ptr s)) \<and> is_subject aag (fst slot)) \<and> (\<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits \<longrightarrow> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of rv) (bits_of rv) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of rv) (bits_of rv) f) slot s)) s \<and> (cte_wp_at (\<lambda>a. is_untyped_cap rv \<and> (\<exists>idx. a = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot s \<and> fst slot \<notin> {obj_ref_of rv..obj_ref_of rv + 2 ^ bits_of rv - 1}) \<and> (pspace_aligned and valid_objs and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> obj_ref_of cp = obj_ref_of rv \<and> bits_of cp = bits_of rv) slot s) and K (untyped_range rv \<subseteq> {obj_ref_of rv..obj_ref_of rv + 2 ^ bits_of rv - 1})) s \<and> (only_timer_irq_inv irq st and (\<lambda>_. True) and (\<lambda>_. True)) s \<and> descendants_of slot (cdt s) = {}))\<rbrace>, -
 3. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> ?P'10 s \<and> ?P''10 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''10\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (free_index_of rv = 0 \<longrightarrow> True) \<and> (free_index_of rv \<noteq> 0 \<longrightarrow> (arm_global_pd (arch_state s) \<notin> ptr_range (obj_ref_of rv) (bits_of rv) \<and> idle_thread s \<notin> ptr_range (obj_ref_of rv) (bits_of rv) \<and> is_aligned (obj_ref_of rv) (bits_of rv) \<and> 2 \<le> bits_of rv \<and> bits_of rv < word_bits) \<and> (is_device_untyped_cap rv \<longrightarrow> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of rv) (bits_of rv) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of rv) (bits_of rv) f) slot s)) s \<and> (invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {obj_ref_of rv..obj_ref_of rv + 2 ^ bits_of rv - 1}) ptr s)) \<and> is_subject aag (fst slot)) \<and> (bits_of rv < resetChunkBits \<longrightarrow> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of rv) (bits_of rv) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of rv) (bits_of rv) f) slot s)) s \<and> (invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {obj_ref_of rv..obj_ref_of rv + 2 ^ bits_of rv - 1}) ptr s)) \<and> is_subject aag (fst slot)) \<and> (\<not> is_device_untyped_cap rv \<and> \<not> bits_of rv < resetChunkBits \<longrightarrow> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of rv) (bits_of rv) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of rv) (bits_of rv) f) slot s)) s \<and> (cte_wp_at (\<lambda>a. is_untyped_cap rv \<and> (\<exists>idx. a = free_index_update (\<lambda>_. idx) rv) \<and> free_index_of rv \<le> 2 ^ bits_of rv \<and> is_subject aag (fst slot)) slot s \<and> fst slot \<notin> {obj_ref_of rv..obj_ref_of rv + 2 ^ bits_of rv - 1}) \<and> (pspace_aligned and valid_objs and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> obj_ref_of cp = obj_ref_of rv \<and> bits_of cp = bits_of rv) slot s) and K (untyped_range rv \<subseteq> {obj_ref_of rv..obj_ref_of rv + 2 ^ bits_of rv - 1})) s \<and> (only_timer_irq_inv irq st and (\<lambda>_. True) and (\<lambda>_. True)) s \<and> descendants_of slot (cdt s) = {}))\<rbrace>, -
 2. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> K (is_subject aag (fst slot)) s \<and> ?P''10 s proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s \<and> only_timer_irq_inv irq st s \<and> is_subject aag (fst slot) \<and> descendants_of slot (cdt s) = {} \<Longrightarrow> K (is_subject aag (fst slot)) s \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (free_index_of cap = 0 \<longrightarrow> True) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> (arm_global_pd (arch_state s) \<notin> ptr_range (obj_ref_of cap) (bits_of cap) \<and> idle_thread s \<notin> ptr_range (obj_ref_of cap) (bits_of cap) \<and> is_aligned (obj_ref_of cap) (bits_of cap) \<and> 2 \<le> bits_of cap \<and> bits_of cap < word_bits) \<and> (is_device_untyped_cap cap \<longrightarrow> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of cap) (bits_of cap) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of cap) (bits_of cap) f) slot s)) s \<and> (invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1}) ptr s)) \<and> is_subject aag (fst slot)) \<and> (bits_of cap < resetChunkBits \<longrightarrow> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of cap) (bits_of cap) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of cap) (bits_of cap) f) slot s)) s \<and> (invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1}) ptr s)) \<and> is_subject aag (fst slot)) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits \<longrightarrow> (invs and ct_active and (\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (UntypedCap dev (obj_ref_of cap) (bits_of cap) f)) slot s \<and> descendants_range (UntypedCap dev (obj_ref_of cap) (bits_of cap) f) slot s)) s \<and> (cte_wp_at (\<lambda>a. is_untyped_cap cap \<and> (\<exists>idx. a = free_index_update (\<lambda>_. idx) cap) \<and> free_index_of cap \<le> 2 ^ bits_of cap \<and> is_subject aag (fst slot)) slot s \<and> fst slot \<notin> {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1}) \<and> (pspace_aligned and valid_objs and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> obj_ref_of cp = obj_ref_of cap \<and> bits_of cp = bits_of cap) slot s) and K (untyped_range cap \<subseteq> {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1})) s \<and> (only_timer_irq_inv irq st and (\<lambda>_. True) and (\<lambda>_. True)) s \<and> descendants_of slot (cdt s) = {}))) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); 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> 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> 2 \<le> bits \<and> bits < word_bits \<and> (dev \<longrightarrow> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f) \<and> descendants_range (UntypedCap dev r bits f) (a, b) 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> (bits < resetChunkBits \<longrightarrow> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f) \<and> descendants_range (UntypedCap dev r bits f) (a, b) 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> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f) \<and> descendants_range (UntypedCap dev r bits f) (a, b) s) \<and> free_index_of (UntypedCap False r bits f) \<le> 2 ^ bits \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pspace_aligned s \<and> valid_objs 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> obj_ref_of cap = r \<and> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) = bits)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); 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> 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> 2 \<le> bits \<and> bits < word_bits \<and> (dev \<longrightarrow> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f) \<and> descendants_range (UntypedCap dev r bits f) (a, b) 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> (bits < resetChunkBits \<longrightarrow> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f) \<and> descendants_range (UntypedCap dev r bits f) (a, b) 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> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f) \<and> descendants_range (UntypedCap dev r bits f) (a, b) s) \<and> free_index_of (UntypedCap False r bits f) \<le> 2 ^ bits \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pspace_aligned s \<and> valid_objs 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> obj_ref_of cap = r \<and> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) = bits)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<notin> ptr_range r bits \<and> idle_thread s \<notin> ptr_range r bits \<and> 2 \<le> bits \<and> (dev \<longrightarrow> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f) \<and> descendants_range (UntypedCap dev r bits f) (a, b) 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> (bits < resetChunkBits \<longrightarrow> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f) \<and> descendants_range (UntypedCap dev r bits f) (a, b) 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> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f) \<and> descendants_range (UntypedCap dev r bits f) (a, b) s) \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pspace_aligned s \<and> valid_objs 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> obj_ref_of cap = r \<and> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) = bits)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; global_refs s \<inter> {r..r + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<notin> ptr_range r bits \<and> idle_thread s \<notin> ptr_range r bits \<and> 2 \<le> bits \<and> (dev \<longrightarrow> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f) \<and> descendants_range (UntypedCap dev r bits f) (a, b) 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> (bits < resetChunkBits \<longrightarrow> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f) \<and> descendants_range (UntypedCap dev r bits f) (a, b) 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> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> (\<exists>a b dev f. caps_of_state s (a, b) = Some (UntypedCap dev r bits f) \<and> descendants_range (UntypedCap dev r bits f) (a, b) s) \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pspace_aligned s \<and> valid_objs 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> obj_ref_of cap = r \<and> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) = bits)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<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> 2 \<le> bits \<and> (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> (\<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_in (cap_range cap) (a, b) s \<and> untyped_range cap = ptr_range r bits)) \<and> (bits < resetChunkBits \<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> (\<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_in (cap_range cap) (a, b) s \<and> untyped_range cap = ptr_range r bits)) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<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> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pspace_aligned s \<and> valid_objs 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> obj_ref_of cap = r \<and> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) = bits)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<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 = {}; ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev r bits f)) slot s\<rbrakk> \<Longrightarrow> 2 \<le> bits \<and> (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> (\<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_in (cap_range cap) (a, b) s \<and> untyped_range cap = ptr_range r bits)) \<and> (bits < resetChunkBits \<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> (\<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_in (cap_range cap) (a, b) s \<and> untyped_range cap = ptr_range r bits)) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<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> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> pspace_aligned s \<and> valid_objs 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> obj_ref_of cap = r \<and> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) = bits)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<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 = {}; ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev r bits f)) slot s\<rbrakk> \<Longrightarrow> 2 \<le> bits \<and> (dev \<longrightarrow> {r..r + 2 ^ bits - 1} = ptr_range r bits) \<and> (bits < resetChunkBits \<longrightarrow> {r..r + 2 ^ bits - 1} = ptr_range r bits) \<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> valid_objs s) proof (prove)
goal (4 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<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> descendants_range_in (untyped_range (UntypedCap dev r bits f)) slot s
 2. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<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> untyped_children_in_mdb s
 3. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<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> valid_global_refs s
 4. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<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 = {}; fst slot \<notin> untyped_range (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> 2 \<le> bits \<and> (dev \<longrightarrow> {r..r + 2 ^ bits - 1} = ptr_range r bits) \<and> (bits < resetChunkBits \<longrightarrow> {r..r + 2 ^ bits - 1} = ptr_range r bits) \<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> valid_objs s) proof (prove)
goal (3 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<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> untyped_children_in_mdb s
 2. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<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> valid_global_refs s
 3. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<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 = {}; fst slot \<notin> untyped_range (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> 2 \<le> bits \<and> (dev \<longrightarrow> {r..r + 2 ^ bits - 1} = ptr_range r bits) \<and> (bits < resetChunkBits \<longrightarrow> {r..r + 2 ^ bits - 1} = ptr_range r bits) \<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> valid_objs s) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>invs s; ct_active s; only_timer_irq_inv irq st s; is_subject aag (fst slot); descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<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 = {}; r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> 2 \<le> bits \<and> (dev \<longrightarrow> {r..r + 2 ^ bits - 1} = ptr_range r bits) \<and> (bits < resetChunkBits \<longrightarrow> {r..r + 2 ^ bits - 1} = ptr_range r bits) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> pspace_aligned s \<and> valid_objs s) proof (prove)
goal:
No subgoals!