theory FinalCaps

lemma reset_untyped_cap_silc_inv:
  "\<lbrace>silc_inv aag st and cte_wp_at is_untyped_cap slot
                    and invs and pas_refined aag
                    and (\<lambda>s. descendants_of slot (cdt s) = {})
                    and K (is_subject aag (fst slot))\<rbrace>
   reset_untyped_cap slot
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: reset_untyped_cap_def cong: if_cong) apply (rule validE_valid, rule hoare_pre) apply (wp set_cap_silc_inv_simple | simp add: unless_def)+ apply (rule valid_validE, rule_tac Q="\<lambda>_. cte_wp_at is_untyped_cap slot and
                                               silc_inv aag st" in hoare_strengthen_post) apply (rule validE_valid, rule mapME_x_inv_wp, rule hoare_pre) apply (wp mapME_x_inv_wp preemption_point_inv set_cap_cte_wp_at
                 set_cap_silc_inv_simple | simp)+ apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps) apply simp apply (wp hoare_vcg_const_imp_lift delete_objects_silc_inv get_cap_wp
              set_cap_silc_inv_simple
           | simp add: if_apply_def2)+ apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def) apply (frule(1) cap_auth_caps_of_state) apply (clarsimp simp: aag_cap_auth_def aag_has_Control_iff_owns
                        ptr_range_def[symmetric]) apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], 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+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and cte_wp_at is_untyped_cap slot and invs and pas_refined aag and (\<lambda>s. descendants_of slot (cdt s) = {}) and K (is_subject aag (fst slot))\<rbrace> reset_untyped_cap slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>silc_inv aag st and cte_wp_at is_untyped_cap slot and invs and pas_refined aag and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> reset_untyped_cap slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>silc_inv aag st and cte_wp_at is_untyped_cap slot and invs and pas_refined aag and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE cap <- liftE (get_cap slot);
if free_index_of cap = 0 then returnOk () else doE y <- liftE (delete_objects (obj_ref_of cap) (bits_of cap));
if is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits then liftE (do y <- unless (is_device_untyped_cap cap) (do_machine_op (clearMemory (obj_ref_of cap) (2 ^ bits_of cap)));
set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) slot
od) else mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)]))
odE
odE \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q8\<rbrace> doE cap <- liftE (get_cap slot);
if free_index_of cap = 0 then returnOk () else doE y <- liftE (delete_objects (obj_ref_of cap) (bits_of cap));
if is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits then liftE (do y <- unless (is_device_untyped_cap cap) (do_machine_op (clearMemory (obj_ref_of cap) (2 ^ bits_of cap)));
set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) slot
od) else mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)]))
odE
odE \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and cte_wp_at is_untyped_cap slot and invs and pas_refined aag and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits\<rbrakk> \<Longrightarrow> \<lbrace>?R16 cap ()\<rbrace> mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)])) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R13 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. silc_inv aag st s \<and> cte_wp_at (\<lambda>cp. cap_irqs cp = cap_irqs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) \<and> obj_refs cp = obj_refs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) slot s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. silc_inv aag st s \<and> cte_wp_at (\<lambda>a. cap_irqs a = cap_irqs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) \<and> obj_refs a = obj_refs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) slot s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> ?R16 cap y s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q8\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> silc_inv aag st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R13 cap s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and cte_wp_at is_untyped_cap slot and invs and pas_refined aag and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (5 subgoals):
 1. \<And>cap. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits\<rbrakk> \<Longrightarrow> \<lbrace>?R16 cap ()\<rbrace> mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)])) \<lbrace>\<lambda>_. cte_wp_at is_untyped_cap slot and silc_inv aag st\<rbrace>
 2. \<And>cap rv s. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; (cte_wp_at is_untyped_cap slot and silc_inv aag st) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 3. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R13 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. silc_inv aag st s \<and> cte_wp_at (\<lambda>cp. cap_irqs cp = cap_irqs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) \<and> obj_refs cp = obj_refs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) slot s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. silc_inv aag st s \<and> cte_wp_at (\<lambda>a. cap_irqs a = cap_irqs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) \<and> obj_refs a = obj_refs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) slot s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> ?R16 cap y s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q8\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> silc_inv aag st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R13 cap s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and cte_wp_at is_untyped_cap slot and invs and pas_refined aag and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (6 subgoals):
 1. \<And>cap x. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits\<rbrakk> \<Longrightarrow> \<lbrace>?Q37 cap x\<rbrace> doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of cap) (bits_of cap) (x * 2 ^ resetChunkBits)) slot);
preemption_point
odE \<lbrace>\<lambda>_. cte_wp_at is_untyped_cap slot and silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. cte_wp_at is_untyped_cap slot and silc_inv aag st\<rbrace>
 2. \<And>cap x s. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; (cte_wp_at is_untyped_cap slot and silc_inv aag st) s\<rbrakk> \<Longrightarrow> ?Q37 cap x s
 3. \<And>cap rv s. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; (cte_wp_at is_untyped_cap slot and silc_inv aag st) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 4. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R13 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. silc_inv aag st s \<and> cte_wp_at (\<lambda>cp. cap_irqs cp = cap_irqs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) \<and> obj_refs cp = obj_refs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) slot s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. silc_inv aag st s \<and> cte_wp_at (\<lambda>a. cap_irqs a = cap_irqs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) \<and> obj_refs a = obj_refs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) slot s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (cte_wp_at is_untyped_cap slot and silc_inv aag st) s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q8\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> silc_inv aag st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R13 cap s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and cte_wp_at is_untyped_cap slot and invs and pas_refined aag and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (5 subgoals):
 1. \<And>cap s. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; cte_wp_at is_untyped_cap slot s \<and> silc_inv aag st s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s \<and> cte_wp_at (\<lambda>a. cap_irqs a = {} \<and> obj_refs a = {}) slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> cte_wp_at (\<lambda>a. cap_irqs a = {} \<and> obj_refs a = {}) slot s
 2. \<And>cap rv s. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; (cte_wp_at is_untyped_cap slot and silc_inv aag st) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 3. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R13 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. silc_inv aag st s \<and> cte_wp_at (\<lambda>cp. cap_irqs cp = cap_irqs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) \<and> obj_refs cp = obj_refs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) slot s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. silc_inv aag st s \<and> cte_wp_at (\<lambda>a. cap_irqs a = cap_irqs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) \<and> obj_refs a = obj_refs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) slot s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (cte_wp_at is_untyped_cap slot and silc_inv aag st) s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q8\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> silc_inv aag st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R13 cap s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and cte_wp_at is_untyped_cap slot and invs and pas_refined aag and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (4 subgoals):
 1. \<And>cap rv s. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; (cte_wp_at is_untyped_cap slot and silc_inv aag st) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R13 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. silc_inv aag st s \<and> cte_wp_at (\<lambda>cp. cap_irqs cp = cap_irqs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) \<and> obj_refs cp = obj_refs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) slot s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. silc_inv aag st s \<and> cte_wp_at (\<lambda>a. cap_irqs a = cap_irqs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) \<and> obj_refs a = obj_refs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) slot s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (cte_wp_at is_untyped_cap slot and silc_inv aag st) s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q8\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> silc_inv aag st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R13 cap s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and cte_wp_at is_untyped_cap slot and invs and pas_refined aag and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (3 subgoals):
 1. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R13 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. silc_inv aag st s \<and> cte_wp_at (\<lambda>cp. cap_irqs cp = cap_irqs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) \<and> obj_refs cp = obj_refs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) slot s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. silc_inv aag st s \<and> cte_wp_at (\<lambda>a. cap_irqs a = cap_irqs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) \<and> obj_refs a = obj_refs (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) slot s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (cte_wp_at is_untyped_cap slot and silc_inv aag st) s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q8\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> silc_inv aag st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R13 cap s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and cte_wp_at is_untyped_cap slot and invs and pas_refined aag and (\<lambda>s. descendants_of slot (cdt s) = {})) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s \<and> cte_wp_at is_untyped_cap slot s \<and> invs s \<and> pas_refined aag s \<and> descendants_of slot (cdt s) = {}\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> 0 < free_index_of cap \<longrightarrow> (is_device_untyped_cap cap \<longrightarrow> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). is_subject aag p) \<and> cte_wp_at (\<lambda>a. cap_irqs a = {} \<and> obj_refs a = {}) slot s \<and> (obj_ref_of cap \<le> fst slot \<longrightarrow> \<not> fst slot \<le> obj_ref_of cap + 2 ^ bits_of cap - 1)) \<and> (bits_of cap < resetChunkBits \<longrightarrow> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). is_subject aag p) \<and> cte_wp_at (\<lambda>a. cap_irqs a = {} \<and> obj_refs a = {}) slot s \<and> (obj_ref_of cap \<le> fst slot \<longrightarrow> \<not> fst slot \<le> obj_ref_of cap + 2 ^ bits_of cap - 1)) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits \<longrightarrow> (obj_ref_of cap \<le> fst slot \<longrightarrow> \<not> fst slot \<le> obj_ref_of cap + 2 ^ bits_of cap - 1) \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). is_subject aag p)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; invs s; pas_refined aag s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> (\<forall>p\<in>ptr_range r bits. is_subject aag p) \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1)) \<and> (bits < resetChunkBits \<longrightarrow> (\<forall>p\<in>ptr_range r bits. is_subject aag p) \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1)) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> (\<forall>p\<in>ptr_range r bits. is_subject aag p)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; invs s; pas_refined aag s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); aag_cap_auth aag (pasObjectAbs aag (fst slot)) (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> (\<forall>p\<in>ptr_range r bits. is_subject aag p) \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1)) \<and> (bits < resetChunkBits \<longrightarrow> (\<forall>p\<in>ptr_range r bits. is_subject aag p) \<and> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1)) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> (r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> (\<forall>p\<in>ptr_range r bits. is_subject aag p)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; invs s; pas_refined aag s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); \<forall>x\<in>ptr_range r bits. is_subject aag x; cap_links_asid_slot aag (pasSubject aag) (UntypedCap dev r bits f); cap_links_irq aag (pasSubject aag) (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> (bits < resetChunkBits \<longrightarrow> r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; invs s; pas_refined aag s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); \<forall>x\<in>ptr_range r bits. is_subject aag x; cap_links_asid_slot aag (pasSubject aag) (UntypedCap dev r bits f); cap_links_irq aag (pasSubject aag) (UntypedCap dev r bits f); ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev r bits f)) slot s\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> (bits < resetChunkBits \<longrightarrow> r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) proof (prove)
goal (4 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; invs s; pas_refined aag s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); \<forall>x\<in>ptr_range r bits. is_subject aag x; cap_links_asid_slot aag (pasSubject aag) (UntypedCap dev r bits f); cap_links_irq aag (pasSubject aag) (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> descendants_range_in (untyped_range (UntypedCap dev r bits f)) slot s
 2. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; invs s; pas_refined aag s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); \<forall>x\<in>ptr_range r bits. is_subject aag x; cap_links_asid_slot aag (pasSubject aag) (UntypedCap dev r bits f); cap_links_irq aag (pasSubject aag) (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 3. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; invs s; pas_refined aag s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); \<forall>x\<in>ptr_range r bits. is_subject aag x; cap_links_asid_slot aag (pasSubject aag) (UntypedCap dev r bits f); cap_links_irq aag (pasSubject aag) (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> valid_global_refs s
 4. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; invs s; pas_refined aag s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); \<forall>x\<in>ptr_range r bits. is_subject aag x; cap_links_asid_slot aag (pasSubject aag) (UntypedCap dev r bits f); cap_links_irq aag (pasSubject aag) (UntypedCap dev r bits f); fst slot \<notin> untyped_range (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> (bits < resetChunkBits \<longrightarrow> r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) proof (prove)
goal (3 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; invs s; pas_refined aag s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); \<forall>x\<in>ptr_range r bits. is_subject aag x; cap_links_asid_slot aag (pasSubject aag) (UntypedCap dev r bits f); cap_links_irq aag (pasSubject aag) (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 2. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; invs s; pas_refined aag s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); \<forall>x\<in>ptr_range r bits. is_subject aag x; cap_links_asid_slot aag (pasSubject aag) (UntypedCap dev r bits f); cap_links_irq aag (pasSubject aag) (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> valid_global_refs s
 3. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; invs s; pas_refined aag s; descendants_of slot (cdt s) = {}; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); \<forall>x\<in>ptr_range r bits. is_subject aag x; cap_links_asid_slot aag (pasSubject aag) (UntypedCap dev r bits f); cap_links_irq aag (pasSubject aag) (UntypedCap dev r bits f); fst slot \<notin> untyped_range (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> (bits < resetChunkBits \<longrightarrow> r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> r \<le> fst slot \<longrightarrow> \<not> fst slot \<le> r + 2 ^ bits - 1) proof (prove)
goal:
No subgoals!