theory Retype_AC

lemma reset_untyped_cap_pspace_aligned[wp]:
  "reset_untyped_cap slot \<lbrace>pspace_aligned\<rbrace>" apply (clarsimp simp: reset_untyped_cap_def) apply (wpsimp wp: mapME_x_inv_wp ) apply (rule valid_validE) apply (wpsimp wp: preemption_point_inv dxo_wp_weak hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> reset_untyped_cap slot \<lbrace>\<lambda>_. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<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>_. pspace_aligned\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>cap x. \<lbrakk>0 < free_index_of cap; \<not> is_device_untyped_cap cap; \<not> bits_of cap < resetChunkBits\<rbrakk> \<Longrightarrow> \<lbrace>?B21 cap () x () ()\<rbrace> preemption_point \<lbrace>\<lambda>_. pspace_aligned\<rbrace>, \<lbrace>\<lambda>_. pspace_aligned\<rbrace>
 2. \<And>cap y x ya. \<lbrakk>free_index_of cap \<noteq> 0; \<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits)\<rbrakk> \<Longrightarrow> \<lbrace>?B20 cap y x ya\<rbrace> liftE (set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) (x * 2 ^ resetChunkBits)) slot) \<lbrace>?B21 cap y x ya\<rbrace>, \<lbrace>\<lambda>_. pspace_aligned\<rbrace>
 3. \<And>cap y x. \<lbrakk>free_index_of cap \<noteq> 0; \<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits)\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned\<rbrace> liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits))) \<lbrace>?B20 cap y x\<rbrace>, \<lbrace>\<lambda>_. pspace_aligned\<rbrace>
 4. \<And>cap. free_index_of cap \<noteq> 0 \<Longrightarrow> \<lbrace>?R10 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 pspace_aligned else pspace_aligned) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> pspace_aligned s)\<rbrace>, \<lbrace>\<lambda>_. pspace_aligned\<rbrace>
 5. \<lbrace>?Q7\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> pspace_aligned s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R10 cap s)\<rbrace>, \<lbrace>\<lambda>_. pspace_aligned\<rbrace>
 6. \<And>s. pspace_aligned s \<Longrightarrow> ?Q7 s proof (prove)
goal (6 subgoals):
 1. \<And>cap x. \<lbrakk>0 < free_index_of cap; \<not> is_device_untyped_cap cap; \<not> bits_of cap < resetChunkBits\<rbrakk> \<Longrightarrow> \<lbrace>?B21 cap () x () ()\<rbrace> preemption_point \<lbrace>\<lambda>_. pspace_aligned\<rbrace>
 2. \<And>cap y x ya. \<lbrakk>free_index_of cap \<noteq> 0; \<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits)\<rbrakk> \<Longrightarrow> \<lbrace>?B20 cap y x ya\<rbrace> liftE (set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) (x * 2 ^ resetChunkBits)) slot) \<lbrace>?B21 cap y x ya\<rbrace>, \<lbrace>\<lambda>_. pspace_aligned\<rbrace>
 3. \<And>cap y x. \<lbrakk>free_index_of cap \<noteq> 0; \<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits)\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned\<rbrace> liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat x << resetChunkBits)) (2 ^ resetChunkBits))) \<lbrace>?B20 cap y x\<rbrace>, \<lbrace>\<lambda>_. pspace_aligned\<rbrace>
 4. \<And>cap. free_index_of cap \<noteq> 0 \<Longrightarrow> \<lbrace>?R10 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 pspace_aligned else pspace_aligned) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> pspace_aligned s)\<rbrace>, \<lbrace>\<lambda>_. pspace_aligned\<rbrace>
 5. \<lbrace>?Q7\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> pspace_aligned s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R10 cap s)\<rbrace>, \<lbrace>\<lambda>_. pspace_aligned\<rbrace>
 6. \<And>s. pspace_aligned s \<Longrightarrow> ?Q7 s proof (prove)
goal:
No subgoals!