theory ArchDetype_AI

lemma delete_objects_invs[wp]:
  "\<lbrace>(\<lambda>s. \<exists>slot. cte_wp_at ((=) (cap.UntypedCap dev ptr bits f)) slot s
    \<and> descendants_range (cap.UntypedCap dev ptr bits f) slot s) and
    invs and ct_active\<rbrace>
    delete_objects ptr bits \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: delete_objects_def) apply (simp add: freeMemory_def word_size_def bind_assoc
                   empty_fail_mapM_x ef_storeWord) apply (rule hoare_pre) apply (rule_tac G="is_aligned ptr bits \<and> word_size_bits \<le> bits \<and> bits \<le> word_bits"
                in hoare_grab_asm) apply (simp add: mapM_storeWord_clear_um[unfolded word_size_def]
                    intvl_range_conv[where 'a=machine_word_len, folded word_bits_def]) apply wp apply clarsimp apply (frule invs_untyped_children) apply (frule detype_invariants, clarsimp+) apply (drule invs_valid_objs) apply (drule (1) cte_wp_valid_cap) apply (simp add: valid_cap_def cap_aligned_def word_size_bits_def untyped_min_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>slot. cte_wp_at ((=) (UntypedCap dev ptr bits f)) slot s \<and> descendants_range (UntypedCap dev ptr bits f) slot s) and invs and ct_active\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>a b. cte_wp_at ((=) (UntypedCap dev ptr bits f)) (a, b) s \<and> descendants_range (UntypedCap dev ptr bits f) (a, b) s) and invs and ct_active\<rbrace> do y <- do_machine_op (freeMemory ptr bits);
modify (detype {ptr..ptr + 2 ^ bits - 1})
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>a b. cte_wp_at ((=) (UntypedCap dev ptr bits f)) (a, b) s \<and> descendants_range (UntypedCap dev ptr bits f) (a, b) s) and invs and ct_active\<rbrace> do y <- do_machine_op (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + 4 .e. ptr + 2 ^ bits - 1]);
modify (detype {ptr..ptr + 2 ^ bits - 1})
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do y <- do_machine_op (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + 4 .e. ptr + 2 ^ bits - 1]);
modify (detype {ptr..ptr + 2 ^ bits - 1})
od \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>a b. cte_wp_at ((=) (UntypedCap dev ptr bits f)) (a, b) s \<and> descendants_range (UntypedCap dev ptr bits f) (a, b) s) and invs and ct_active) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. is_aligned ptr bits \<and> word_size_bits \<le> bits \<and> bits \<le> word_bits \<Longrightarrow> \<lbrace>?P3\<rbrace> do y <- do_machine_op (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + 4 .e. ptr + 2 ^ bits - 1]);
modify (detype {ptr..ptr + 2 ^ bits - 1})
od \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>a b. cte_wp_at ((=) (UntypedCap dev ptr bits f)) (a, b) s \<and> descendants_range (UntypedCap dev ptr bits f) (a, b) s) and invs and ct_active) s \<Longrightarrow> (is_aligned ptr bits \<and> word_size_bits \<le> bits \<and> bits \<le> word_bits) \<and> ?P3 s proof (prove)
goal (2 subgoals):
 1. is_aligned ptr bits \<and> word_size_bits \<le> bits \<and> bits \<le> word_bits \<Longrightarrow> \<lbrace>?P3\<rbrace> do y <- modify (clear_um {ptr..ptr + 2 ^ bits - 1});
modify (detype {ptr..ptr + 2 ^ bits - 1})
od \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>a b. cte_wp_at ((=) (UntypedCap dev ptr bits f)) (a, b) s \<and> descendants_range (UntypedCap dev ptr bits f) (a, b) s) and invs and ct_active) s \<Longrightarrow> (is_aligned ptr bits \<and> word_size_bits \<le> bits \<and> bits \<le> word_bits) \<and> ?P3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<exists>a b. cte_wp_at ((=) (UntypedCap dev ptr bits f)) (a, b) s \<and> descendants_range (UntypedCap dev ptr bits f) (a, b) s) and invs and ct_active) s \<Longrightarrow> (is_aligned ptr bits \<and> word_size_bits \<le> bits \<and> bits \<le> word_bits) \<and> invs (detype {ptr..ptr + 2 ^ bits - 1} (clear_um {ptr..ptr + 2 ^ bits - 1} s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>invs s; ct_active s; cte_wp_at ((=) (UntypedCap dev ptr bits f)) (a, b) s; descendants_range (UntypedCap dev ptr bits f) (a, b) s\<rbrakk> \<Longrightarrow> is_aligned ptr bits \<and> word_size_bits \<le> bits \<and> bits \<le> word_bits \<and> invs (detype {ptr..ptr + 2 ^ bits - 1} (clear_um {ptr..ptr + 2 ^ bits - 1} s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>invs s; ct_active s; cte_wp_at ((=) (UntypedCap dev ptr bits f)) (a, b) s; descendants_range (UntypedCap dev ptr bits f) (a, b) s; untyped_children_in_mdb s\<rbrakk> \<Longrightarrow> is_aligned ptr bits \<and> word_size_bits \<le> bits \<and> bits \<le> word_bits \<and> invs (detype {ptr..ptr + 2 ^ bits - 1} (clear_um {ptr..ptr + 2 ^ bits - 1} s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>invs s; ct_active s; cte_wp_at ((=) (UntypedCap dev ptr bits f)) (a, b) s; descendants_range (UntypedCap dev ptr bits f) (a, b) s; untyped_children_in_mdb s; invs (detype {ptr..ptr + 2 ^ bits - 1} (clear_um {ptr..ptr + 2 ^ bits - 1} s)); untyped_children_in_mdb (detype {ptr..ptr + 2 ^ bits - 1} (clear_um {ptr..ptr + 2 ^ bits - 1} s))\<rbrakk> \<Longrightarrow> is_aligned ptr bits \<and> word_size_bits \<le> bits \<and> bits \<le> word_bits proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>ct_active s; cte_wp_at ((=) (UntypedCap dev ptr bits f)) (a, b) s; descendants_range (UntypedCap dev ptr bits f) (a, b) s; untyped_children_in_mdb s; invs (detype {ptr..ptr + 2 ^ bits - 1} (clear_um {ptr..ptr + 2 ^ bits - 1} s)); untyped_children_in_mdb (detype {ptr..ptr + 2 ^ bits - 1} (clear_um {ptr..ptr + 2 ^ bits - 1} s)); valid_objs s\<rbrakk> \<Longrightarrow> is_aligned ptr bits \<and> word_size_bits \<le> bits \<and> bits \<le> word_bits proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>ct_active s; descendants_range (UntypedCap dev ptr bits f) (a, b) s; untyped_children_in_mdb s; invs (detype {ptr..ptr + 2 ^ bits - 1} (clear_um {ptr..ptr + 2 ^ bits - 1} s)); untyped_children_in_mdb (detype {ptr..ptr + 2 ^ bits - 1} (clear_um {ptr..ptr + 2 ^ bits - 1} s)); valid_objs s; s \<turnstile> UntypedCap dev ptr bits f\<rbrakk> \<Longrightarrow> is_aligned ptr bits \<and> word_size_bits \<le> bits \<and> bits \<le> word_bits proof (prove)
goal:
No subgoals!