theory Retype_AC

lemma reset_untyped_cap_integrity:
  "\<lbrace>integrity aag X st and pas_refined aag and valid_objs
                       and cte_wp_at is_untyped_cap slot
                       and K (is_subject aag (fst slot))\<rbrace>
   reset_untyped_cap slot
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: reset_untyped_cap_def) apply (rule hoare_pre) apply (wp set_cap_integrity_autarch dmo_clearMemory_respects'
         | simp add: unless_def)+ apply (rule valid_validE) apply (rule_tac P="cap_aligned cap \<and> is_untyped_cap cap \<and>
                        (\<forall>r \<in> cap_range cap. aag_has_auth_to aag Write r)" in hoare_gen_asm) apply (rule validE_valid, rule mapME_x_wp') apply (rule hoare_pre) apply (wp mapME_x_inv_wp[OF hoare_pre(2)]  preemption_point_inv'
                set_cap_integrity_autarch dmo_clearMemory_respects' | simp)+ apply (clarsimp simp: cap_aligned_def is_cap_simps bits_of_def) apply (subst aligned_add_aligned, assumption, rule is_aligned_shiftl, simp+) apply (simp add: word_size_bits_resetChunkBits) apply (clarsimp simp: arg_cong2[where f="(\<le>)", OF refl Kernel_Config.resetChunkBits_def [unfolded atomize_eq]]) apply (drule bspec, erule subsetD[rotated]) apply (simp only: ptr_range_def, rule new_range_subset'; simp add: is_aligned_shiftl) apply (rule shiftl_less_t2n) apply (rule word_of_nat_less) apply simp apply (simp add: word_bits_def) apply clarsimp apply (simp add: if_apply_def2) apply (wp hoare_vcg_const_imp_lift get_cap_wp)+ apply (clarsimp simp: cte_wp_at_caps_of_state) apply (frule caps_of_state_valid_cap, clarsimp+) apply (clarsimp simp: cap_aligned_def is_cap_simps valid_cap_simps bits_of_def) apply (frule(2) cap_cur_auth_caps_of_state) apply (clarsimp simp: aag_cap_auth_def ptr_range_def aag_has_Control_iff_owns
                        pas_refined_refl le_trans[OF word_size_bits_untyped_min_bits]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot and K (is_subject aag (fst slot))\<rbrace> reset_untyped_cap slot \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot\<rbrace> reset_untyped_cap slot \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot\<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>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> doE cap <- liftE (get_cap slot);
if free_index_of cap = 0 then returnOk () else doE y <- liftE (delete_objects (obj_ref_of cap) (bits_of cap));
if is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits then liftE (do y <- unless (is_device_untyped_cap cap) (do_machine_op (clearMemory (obj_ref_of cap) (2 ^ bits_of cap)));
set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) slot
od) else mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)]))
odE
odE \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap ()\<rbrace> mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)])) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> ?R15 cap y s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap ()\<rbrace> mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)])) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> ?R15 cap y s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> \<lbrace>?P'29 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>_. integrity aag X st\<rbrace>
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (?P'29 cap y and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 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; cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag); x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st\<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>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (integrity aag X st and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>cap x. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag); x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)]))\<rbrakk> \<Longrightarrow> \<lbrace>?Q34 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>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X 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; cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag); x \<in> set (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)])); integrity aag X st s\<rbrakk> \<Longrightarrow> ?Q34 cap x s
 3. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (integrity aag X st and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>cap x s. \<lbrakk>is_subject aag (fst slot); \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag); x < 2 ^ (bits_of cap - resetChunkBits) \<and> x * 2 ^ resetChunkBits < free_index_of cap; integrity aag X st s\<rbrakk> \<Longrightarrow> is_aligned (obj_ref_of cap + (word_of_nat x << resetChunkBits)) resetChunkBits \<and> resetChunkBits < word_bits \<and> word_size_bits \<le> resetChunkBits \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap + (word_of_nat x << resetChunkBits)) resetChunkBits. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (integrity aag X st and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>x s dev r bits f. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits; \<forall>r\<in>{r..r + 2 ^ bits - 1}. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_aligned (r + (word_of_nat x << resetChunkBits)) resetChunkBits \<and> word_size_bits \<le> resetChunkBits \<and> (\<forall>p\<in>ptr_range (r + (word_of_nat x << resetChunkBits)) resetChunkBits. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (integrity aag X st and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>x s dev r bits f. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits; \<forall>r\<in>{r..r + 2 ^ bits - 1}. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> word_size_bits \<le> resetChunkBits \<and> (\<forall>p\<in>ptr_range (r + (word_of_nat x << resetChunkBits)) resetChunkBits. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (integrity aag X st and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>x s dev r bits f. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits; \<forall>r\<in>{r..r + 2 ^ bits - 1}. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<forall>p\<in>ptr_range (r + (word_of_nat x << resetChunkBits)) resetChunkBits. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (integrity aag X st and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>x s dev r bits f p. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits; \<forall>r\<in>{r..r + 2 ^ bits - 1}. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag; p \<in> ptr_range (r + (word_of_nat x << resetChunkBits)) resetChunkBits\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (integrity aag X st and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>x s dev r bits f p. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits\<rbrakk> \<Longrightarrow> ptr_range (r + (word_of_nat x << resetChunkBits)) resetChunkBits \<subseteq> {r..r + 2 ^ bits - 1}
 2. \<And>x s dev r bits f p. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits; p \<in> ptr_range (r + (word_of_nat x << resetChunkBits)) resetChunkBits; (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag
 3. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (integrity aag X st and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>x s dev r bits f. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits\<rbrakk> \<Longrightarrow> word_of_nat x << resetChunkBits < 2 ^ bits
 2. \<And>x s dev r bits f p. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits; p \<in> ptr_range (r + (word_of_nat x << resetChunkBits)) resetChunkBits; (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag
 3. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (integrity aag X st and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>x s dev r bits f. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits\<rbrakk> \<Longrightarrow> word_of_nat x < 2 ^ (bits - resetChunkBits)
 2. \<And>x s dev r bits f. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 3. \<And>x s dev r bits f p. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits; p \<in> ptr_range (r + (word_of_nat x << resetChunkBits)) resetChunkBits; (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag
 4. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (integrity aag X st and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 6. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>x s dev r bits f. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits\<rbrakk> \<Longrightarrow> x < unat (2 ^ (bits - resetChunkBits))
 2. \<And>x s dev r bits f. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 3. \<And>x s dev r bits f p. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits; p \<in> ptr_range (r + (word_of_nat x << resetChunkBits)) resetChunkBits; (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag
 4. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (integrity aag X st and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 6. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>x s dev r bits f. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 2. \<And>x s dev r bits f p. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits; p \<in> ptr_range (r + (word_of_nat x << resetChunkBits)) resetChunkBits; (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag
 3. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (integrity aag X st and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>x s dev r bits f p. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; \<not> dev; \<not> bits < resetChunkBits; is_aligned r bits; x < 2 ^ (bits - resetChunkBits); x * 2 ^ resetChunkBits < free_index_of (UntypedCap False r bits f); bits < word_bits; p \<in> ptr_range (r + (word_of_nat x << resetChunkBits)) resetChunkBits; (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag
 2. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (integrity aag X st and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (3 subgoals):
 1. \<And>cap. \<lbrakk>is_subject aag (fst slot); free_index_of cap \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. integrity aag X st s \<and> K (is_subject aag (fst slot)) s else (\<lambda>s. (integrity aag X st and K (is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) s \<and> K (is_subject aag (fst slot)) s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> (integrity aag X st and K (cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (3 subgoals):
 1. \<And>cap. \<lbrakk>is_subject aag (fst slot); 0 < free_index_of cap\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> delete_objects (obj_ref_of cap) (bits_of cap) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<longrightarrow> integrity aag X st s) \<and> (bits_of cap < resetChunkBits \<longrightarrow> (is_device_untyped_cap cap \<longrightarrow> integrity aag X st s) \<and> (\<not> is_device_untyped_cap cap \<longrightarrow> integrity aag X st s \<and> is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits \<longrightarrow> integrity aag X st s \<and> cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))\<rbrace>
 2. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); (integrity aag X st and pas_refined aag and valid_objs and cte_wp_at is_untyped_cap slot) s\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (free_index_of cap = 0 \<longrightarrow> integrity aag X st s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> (is_device_untyped_cap cap \<longrightarrow> integrity aag X st s \<and> is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). is_subject aag p)) \<and> (bits_of cap < resetChunkBits \<longrightarrow> (is_device_untyped_cap cap \<longrightarrow> integrity aag X st s \<and> is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). is_subject aag p)) \<and> (\<not> is_device_untyped_cap cap \<longrightarrow> (integrity aag X st s \<and> is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). is_subject aag p)) \<and> is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits \<longrightarrow> (integrity aag X st s \<and> is_aligned (obj_ref_of cap) (bits_of cap) \<and> bits_of cap < word_bits \<and> word_size_bits \<le> bits_of cap \<and> (\<forall>p\<in>ptr_range (obj_ref_of cap) (bits_of cap). is_subject aag p)) \<and> cap_aligned cap \<and> is_untyped_cap cap \<and> (\<forall>r\<in>cap_range cap. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag))) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; pas_refined aag s; valid_objs s; is_untyped_cap capa; caps_of_state s slot = Some capa; 0 < free_index_of capa\<rbrakk> \<Longrightarrow> (is_device_untyped_cap capa \<longrightarrow> is_aligned (obj_ref_of capa) (bits_of capa) \<and> bits_of capa < word_bits \<and> word_size_bits \<le> bits_of capa \<and> (\<forall>p\<in>ptr_range (obj_ref_of capa) (bits_of capa). is_subject aag p)) \<and> (bits_of capa < resetChunkBits \<longrightarrow> (is_device_untyped_cap capa \<longrightarrow> is_aligned (obj_ref_of capa) (bits_of capa) \<and> bits_of capa < word_bits \<and> word_size_bits \<le> bits_of capa \<and> (\<forall>p\<in>ptr_range (obj_ref_of capa) (bits_of capa). is_subject aag p)) \<and> (\<not> is_device_untyped_cap capa \<longrightarrow> is_aligned (obj_ref_of capa) (bits_of capa) \<and> bits_of capa < word_bits \<and> word_size_bits \<le> bits_of capa \<and> (\<forall>p\<in>ptr_range (obj_ref_of capa) (bits_of capa). is_subject aag p) \<and> is_aligned (obj_ref_of capa) (bits_of capa) \<and> bits_of capa < word_bits \<and> word_size_bits \<le> bits_of capa \<and> (\<forall>p\<in>ptr_range (obj_ref_of capa) (bits_of capa). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) \<and> (\<not> is_device_untyped_cap capa \<and> \<not> bits_of capa < resetChunkBits \<longrightarrow> is_aligned (obj_ref_of capa) (bits_of capa) \<and> bits_of capa < word_bits \<and> word_size_bits \<le> bits_of capa \<and> (\<forall>p\<in>ptr_range (obj_ref_of capa) (bits_of capa). is_subject aag p) \<and> cap_aligned capa \<and> (\<forall>r\<in>untyped_range capa. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; pas_refined aag s; valid_objs s; is_untyped_cap capa; caps_of_state s slot = Some capa; 0 < free_index_of capa; s \<turnstile> capa\<rbrakk> \<Longrightarrow> (is_device_untyped_cap capa \<longrightarrow> is_aligned (obj_ref_of capa) (bits_of capa) \<and> bits_of capa < word_bits \<and> word_size_bits \<le> bits_of capa \<and> (\<forall>p\<in>ptr_range (obj_ref_of capa) (bits_of capa). is_subject aag p)) \<and> (bits_of capa < resetChunkBits \<longrightarrow> (is_device_untyped_cap capa \<longrightarrow> is_aligned (obj_ref_of capa) (bits_of capa) \<and> bits_of capa < word_bits \<and> word_size_bits \<le> bits_of capa \<and> (\<forall>p\<in>ptr_range (obj_ref_of capa) (bits_of capa). is_subject aag p)) \<and> (\<not> is_device_untyped_cap capa \<longrightarrow> is_aligned (obj_ref_of capa) (bits_of capa) \<and> bits_of capa < word_bits \<and> word_size_bits \<le> bits_of capa \<and> (\<forall>p\<in>ptr_range (obj_ref_of capa) (bits_of capa). is_subject aag p) \<and> is_aligned (obj_ref_of capa) (bits_of capa) \<and> bits_of capa < word_bits \<and> word_size_bits \<le> bits_of capa \<and> (\<forall>p\<in>ptr_range (obj_ref_of capa) (bits_of capa). (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) \<and> (\<not> is_device_untyped_cap capa \<and> \<not> bits_of capa < resetChunkBits \<longrightarrow> is_aligned (obj_ref_of capa) (bits_of capa) \<and> bits_of capa < word_bits \<and> word_size_bits \<le> bits_of capa \<and> (\<forall>p\<in>ptr_range (obj_ref_of capa) (bits_of capa). is_subject aag p) \<and> cap_aligned capa \<and> (\<forall>r\<in>untyped_range capa. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; pas_refined aag s; valid_objs s; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range r bits. is_subject aag p)) \<and> (bits < resetChunkBits \<longrightarrow> (dev \<longrightarrow> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range r bits. is_subject aag p)) \<and> (\<not> dev \<longrightarrow> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range r bits. is_subject aag p) \<and> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range r bits. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range r bits. is_subject aag p) \<and> (\<forall>r\<in>{r..r + 2 ^ bits - 1}. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>is_subject aag (fst slot); integrity aag X st s; pas_refined aag s; valid_objs s; caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; pas_cap_cur_auth aag (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range r bits. is_subject aag p)) \<and> (bits < resetChunkBits \<longrightarrow> (dev \<longrightarrow> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range r bits. is_subject aag p)) \<and> (\<not> dev \<longrightarrow> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range r bits. is_subject aag p) \<and> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range r bits. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag))) \<and> (\<not> dev \<and> \<not> bits < resetChunkBits \<longrightarrow> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range r bits. is_subject aag p) \<and> (\<forall>r\<in>{r..r + 2 ^ bits - 1}. (pasSubject aag, Write, pasObjectAbs aag r) \<in> pasPolicy aag)) proof (prove)
goal:
No subgoals!