theory Retype_AC

lemma reset_untyped_cap_valid_arch_state:
  "\<lbrace>\<lambda>s. invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c src_slot s) src_slot s\<rbrace>
   reset_untyped_cap src_slot
   \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" unfolding reset_untyped_cap_def apply (wpsimp wp: mapME_x_inv_wp preemption_point_inv) apply (wp hoare_weak_lift_imp delete_objects_valid_arch_state) apply (wpsimp wp: get_cap_wp)+ apply (cases src_slot) apply (auto simp: cte_wp_at_caps_of_state) apply (fastforce simp: bits_of_def is_cap_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c src_slot s) src_slot s\<rbrace> reset_untyped_cap src_slot \<lbrace>\<lambda>_. valid_arch_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c src_slot s) src_slot s\<rbrace> doE cap <- liftE $ get_cap src_slot;
sz <- returnOk $ bits_of cap;
base <- returnOk $ obj_ref_of cap;
if free_index_of cap = 0 then returnOk () else doE liftE $ delete_objects base sz;
dev <- returnOk $ is_device_untyped_cap cap;
if dev \<or> sz < resetChunkBits then liftE $ do unless dev $ do_machine_op $ clearMemory base (2 ^ sz);
set_cap (UntypedCap dev base sz 0) src_slot
od else mapME_x (\<lambda>i. doE liftE $ do_machine_op $ clearMemory (base + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits);
liftE $ set_cap (UntypedCap dev base sz (i * 2 ^ resetChunkBits)) src_slot;
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (sz - resetChunkBits)]))
odE
odE \<lbrace>\<lambda>_. valid_arch_state\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cap sz base. 0 < free_index_of cap \<Longrightarrow> \<lbrace>?P'101 cap sz base\<rbrace> delete_objects base sz \<lbrace>\<lambda>rv s. (is_device_untyped_cap cap \<longrightarrow> valid_arch_state s) \<and> (sz < resetChunkBits \<longrightarrow> valid_arch_state s) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> sz < resetChunkBits \<longrightarrow> valid_arch_state s)\<rbrace>
 2. \<And>cap sz. \<lbrace>?B4 cap sz\<rbrace> returnOk $ obj_ref_of cap \<lbrace>\<lambda>base s. (free_index_of cap = 0 \<longrightarrow> valid_arch_state s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> True \<and> True \<and> ((\<lambda>s. is_device_untyped_cap cap \<or> sz < resetChunkBits \<longrightarrow> True) and ?P'101 cap sz base) s)\<rbrace>, \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 3. \<And>cap. \<lbrace>?B3 cap\<rbrace> returnOk $ bits_of cap \<lbrace>?B4 cap\<rbrace>, \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 4. \<lbrace>?Q1\<rbrace> liftE $ get_cap src_slot \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 5. \<And>s. invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c src_slot s) src_slot s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>cap sz. \<lbrace>?B4 cap sz\<rbrace> returnOk $ obj_ref_of cap \<lbrace>\<lambda>base s. (free_index_of cap = 0 \<longrightarrow> valid_arch_state s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> True \<and> True \<and> ((\<lambda>s. is_device_untyped_cap cap \<or> sz < resetChunkBits \<longrightarrow> True) and (\<lambda>s. (is_device_untyped_cap cap \<longrightarrow> invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {base..base + 2 ^ sz - 1}) ptr s)) \<and> (sz < resetChunkBits \<longrightarrow> invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {base..base + 2 ^ sz - 1}) ptr s)) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> sz < resetChunkBits \<longrightarrow> invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {base..base + 2 ^ sz - 1}) ptr s)))) s)\<rbrace>, \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 2. \<And>cap. \<lbrace>?B3 cap\<rbrace> returnOk $ bits_of cap \<lbrace>?B4 cap\<rbrace>, \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 3. \<lbrace>?Q1\<rbrace> liftE $ get_cap src_slot \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 4. \<And>s. invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c src_slot s) src_slot s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>invs s; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c src_slot s) src_slot s; cte_wp_at ((=) cap) src_slot s\<rbrakk> \<Longrightarrow> (free_index_of cap = 0 \<longrightarrow> valid_arch_state s) \<and> (0 < free_index_of cap \<longrightarrow> (is_device_untyped_cap cap \<longrightarrow> (\<exists>a b. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (a, b) s \<and> untyped_range c = {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1}) (a, b) s)) \<and> (bits_of cap < resetChunkBits \<longrightarrow> (\<exists>a b. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (a, b) s \<and> untyped_range c = {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1}) (a, b) s)) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits \<longrightarrow> (\<exists>a b. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (a, b) s \<and> untyped_range c = {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1}) (a, b) s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b. \<lbrakk>invs s; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c src_slot s) src_slot s; cte_wp_at ((=) cap) src_slot s; src_slot = (a, b)\<rbrakk> \<Longrightarrow> (free_index_of cap = 0 \<longrightarrow> valid_arch_state s) \<and> (0 < free_index_of cap \<longrightarrow> (is_device_untyped_cap cap \<longrightarrow> (\<exists>a b. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (a, b) s \<and> untyped_range c = {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1}) (a, b) s)) \<and> (bits_of cap < resetChunkBits \<longrightarrow> (\<exists>a b. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (a, b) s \<and> untyped_range c = {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1}) (a, b) s)) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits \<longrightarrow> (\<exists>a b. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (a, b) s \<and> untyped_range c = {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1}) (a, b) s))) proof (prove)
goal (3 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; caps_of_state s (a, b) = Some cap; src_slot = (a, b); is_untyped_cap cap; descendants_range cap (a, b) s; 0 < free_index_of cap; is_device_untyped_cap cap\<rbrakk> \<Longrightarrow> \<exists>a b capa. caps_of_state s (a, b) = Some capa \<and> is_untyped_cap capa \<and> descendants_range capa (a, b) s \<and> untyped_range capa = {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1}
 2. \<And>s cap a b. \<lbrakk>invs s; caps_of_state s (a, b) = Some cap; src_slot = (a, b); is_untyped_cap cap; descendants_range cap (a, b) s; 0 < free_index_of cap; bits_of cap < resetChunkBits\<rbrakk> \<Longrightarrow> \<exists>a b capa. caps_of_state s (a, b) = Some capa \<and> is_untyped_cap capa \<and> descendants_range capa (a, b) s \<and> untyped_range capa = {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1}
 3. \<And>s cap a b. \<lbrakk>invs s; caps_of_state s (a, b) = Some cap; src_slot = (a, b); is_untyped_cap cap; descendants_range cap (a, b) s; 0 < free_index_of cap; \<not> is_device_untyped_cap cap; \<not> bits_of cap < resetChunkBits\<rbrakk> \<Longrightarrow> \<exists>a b capa. caps_of_state s (a, b) = Some capa \<and> is_untyped_cap capa \<and> descendants_range capa (a, b) s \<and> untyped_range capa = {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1} proof (prove)
goal:
No subgoals!