kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_AC

lemma delete_objects_descendants_range_in''':
  "\<lbrace>invs and (\<lambda>s :: det_ext state. \<exists>idx. cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s)
         and descendants_range_in {word2..word2 + 2 ^ sz - 1} slot\<rbrace>
   delete_objects word2 sz
   \<lbrace>\<lambda>_. descendants_range_in {word2 && ~~ mask sz..(word2 && ~~ mask sz) + 2 ^ sz - 1} slot\<rbrace>" apply (clarsimp simp: valid_def) apply (frule untyped_cap_aligned, fastforce) apply (clarsimp) apply (erule use_valid) apply (wp delete_objects_descendants_range_in' | clarsimp | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s) and descendants_range_in {word2..word2 + 2 ^ sz - 1} slot\<rbrace> delete_objects word2 sz \<lbrace>\<lambda>_. descendants_range_in {word2 && ~~ mask sz..(word2 && ~~ mask sz) + 2 ^ sz - 1} slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b idx. \<lbrakk>((), b) \<in> fst (delete_objects word2 sz s); invs s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s\<rbrakk> \<Longrightarrow> descendants_range_in {word2 && ~~ mask sz..(word2 && ~~ mask sz) + 2 ^ sz - 1} slot b proof (prove)
goal (1 subgoal):
 1. \<And>s b idx. \<lbrakk>((), b) \<in> fst (delete_objects word2 sz s); invs s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; is_aligned word2 sz\<rbrakk> \<Longrightarrow> descendants_range_in {word2 && ~~ mask sz..(word2 && ~~ mask sz) + 2 ^ sz - 1} slot b proof (prove)
goal (1 subgoal):
 1. \<And>s b idx. \<lbrakk>((), b) \<in> fst (delete_objects word2 sz s); invs s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; is_aligned word2 sz\<rbrakk> \<Longrightarrow> descendants_range_in {word2..word2 + 2 ^ sz - 1} slot b proof (prove)
goal (2 subgoals):
 1. \<And>s b idx. \<lbrakk>invs s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; is_aligned word2 sz\<rbrakk> \<Longrightarrow> \<lbrace>?P18 s b idx\<rbrace> delete_objects word2 sz \<lbrace>\<lambda>a. descendants_range_in {word2..word2 + 2 ^ sz - 1} slot\<rbrace>
 2. \<And>s b idx. \<lbrakk>invs s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; is_aligned word2 sz\<rbrakk> \<Longrightarrow> ?P18 s b idx s proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma bits_of_UntypedCap:
  "bits_of (UntypedCap dev ptr sz free) = sz" by (simp add: bits_of_def split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bits_of (UntypedCap dev ptr sz free) = sz
theory Retype_AC

lemma delete_objects_pspace_no_overlap:
  "\<lbrace>pspace_aligned and valid_objs and cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot\<rbrace>
   delete_objects ptr sz
   \<lbrace>\<lambda>_. pspace_no_overlap_range_cover ptr sz\<rbrace>" unfolding delete_objects_def do_machine_op_def apply (wp | simp add: split_def detype_machine_state_update_comm)+ apply clarsimp apply (rule pspace_no_overlap_detype) apply (auto dest: cte_wp_at_valid_objs_valid_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_objs and cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot\<rbrace> delete_objects ptr sz \<lbrace>\<lambda>_. pspace_no_overlap (up_aligned_area ptr sz)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_objs and cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot\<rbrace> do do ms <- gets machine_state;
(r, ms') <- select_f (freeMemory ptr sz ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od;
modify (detype {ptr..ptr + 2 ^ sz - 1})
od \<lbrace>\<lambda>_. pspace_no_overlap (up_aligned_area ptr sz)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned s \<and> valid_objs s \<and> cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s \<Longrightarrow> (\<exists>b. ((), b) \<in> fst (freeMemory ptr sz (machine_state s))) \<longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) (detype {ptr..ptr + 2 ^ sz - 1} s) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>pspace_aligned s; valid_objs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s; ((), b) \<in> fst (freeMemory ptr sz (machine_state s))\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) (detype {ptr..ptr + 2 ^ sz - 1} s) proof (prove)
goal (3 subgoals):
 1. \<And>s b. \<lbrakk>pspace_aligned s; valid_objs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s; ((), b) \<in> fst (freeMemory ptr sz (machine_state s))\<rbrakk> \<Longrightarrow> s \<turnstile> UntypedCap (?dev19 s b) ptr sz (?idx19 s b)
 2. \<And>s b. \<lbrakk>pspace_aligned s; valid_objs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s; ((), b) \<in> fst (freeMemory ptr sz (machine_state s))\<rbrakk> \<Longrightarrow> pspace_aligned s
 3. \<And>s b. \<lbrakk>pspace_aligned s; valid_objs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s; ((), b) \<in> fst (freeMemory ptr sz (machine_state s))\<rbrakk> \<Longrightarrow> valid_objs s proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma delete_objects_pspace_no_overlap':
  "\<lbrace>pspace_aligned and valid_objs and cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot\<rbrace>
   delete_objects ptr sz
   \<lbrace>\<lambda>_. pspace_no_overlap_range_cover (ptr && ~~ mask sz) sz\<rbrace>" apply (clarsimp simp: valid_def) apply (frule untyped_cap_aligned, simp) apply (clarsimp) apply (frule(1) cte_wp_at_valid_objs_valid_cap) apply (erule use_valid, wp delete_objects_pspace_no_overlap, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_objs and cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot\<rbrace> delete_objects ptr sz \<lbrace>\<lambda>_. pspace_no_overlap (up_aligned_area (ptr && ~~ mask sz) sz)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (delete_objects ptr sz s); pspace_aligned s; valid_objs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s\<rbrakk> \<Longrightarrow> pspace_no_overlap {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (delete_objects ptr sz s); pspace_aligned s; valid_objs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s; is_aligned ptr sz\<rbrakk> \<Longrightarrow> pspace_no_overlap {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (delete_objects ptr sz s); pspace_aligned s; valid_objs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s; is_aligned ptr sz\<rbrakk> \<Longrightarrow> pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (delete_objects ptr sz s); pspace_aligned s; valid_objs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s; is_aligned ptr sz; \<exists>cap. UntypedCap dev ptr sz idx = cap \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} b proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma valid_cap_range_untyped:
  "\<lbrakk> valid_objs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s \<rbrakk>
     \<Longrightarrow> cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s" apply (rule cte_wp_at_weakenE) apply simp apply (clarsimp simp: word_and_le2 p_assoc_help) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s\<rbrakk> \<Longrightarrow> cte_wp_at ?P slot s
 2. \<And>c. \<lbrakk>valid_objs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s; ?P c\<rbrakk> \<Longrightarrow> up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>valid_objs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s; UntypedCap dev (ptr && ~~ mask sz) sz idx = c\<rbrakk> \<Longrightarrow> up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma aag_cap_auth_UntypedCap_idx_dev:
  "aag_cap_auth aag l (UntypedCap dev base sz idx)
   \<Longrightarrow> aag_cap_auth aag l (UntypedCap dev' base sz idx')" by (clarsimp simp: aag_cap_auth_def cap_links_asid_slot_def
                     cap_links_irq_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. aag_cap_auth aag l (UntypedCap dev base sz idx) \<Longrightarrow> aag_cap_auth aag l (UntypedCap dev' base sz idx')
theory Retype_AC

lemma cte_wp_at_pas_cap_cur_auth_UntypedCap_idx_dev:
  "\<lbrakk> cte_wp_at ((=) (UntypedCap dev base sz idx)) slot s;
     is_subject aag (fst slot); pas_refined aag s\<rbrakk>
     \<Longrightarrow> pas_cap_cur_auth aag (UntypedCap dev' base sz idx')" apply (rule aag_cap_auth_UntypedCap_idx_dev) apply (auto intro: cap_cur_auth_caps_of_state simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (UntypedCap dev base sz idx)) slot s; is_subject aag (fst slot); pas_refined aag s\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag (UntypedCap dev' base sz idx') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (UntypedCap dev base sz idx)) slot s; is_subject aag (fst slot); pas_refined aag s\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag (UntypedCap ?dev base sz ?idx) proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma retype_addrs_aligned_range_cover:
  assumes xin: "x \<in> set (retype_addrs ptr ty n us)"
  and co: "range_cover ptr sz (obj_bits_api ty us) n"
  shows "is_aligned x (obj_bits_api ty us)" using co apply (clarsimp simp: range_cover_def) apply (rule retype_addrs_aligned[OF xin, where sz=sz], simp_all) apply (simp add: word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned x (obj_bits_api ty us) proof (prove)
using this:
range_cover ptr sz (obj_bits_api ty us) n

goal (1 subgoal):
 1. is_aligned x (obj_bits_api ty us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (obj_bits_api ty us); sz < 32; obj_bits_api ty us \<le> sz; n + unat (ptr && mask sz >> obj_bits_api ty us) \<le> 2 ^ (sz - obj_bits_api ty us)\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits_api ty us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (obj_bits_api ty us); sz < 32; obj_bits_api ty us \<le> sz; n + unat (ptr && mask sz >> obj_bits_api ty us) \<le> 2 ^ (sz - obj_bits_api ty us)\<rbrakk> \<Longrightarrow> sz < word_bits proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma pas_refined_work_units_complete[simp]:
  "pas_refined aag (work_units_completed_update f s) = pas_refined aag s" by (simp add: pas_refined_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag (work_units_completed_update f s) = pas_refined aag s
theory Retype_AC

lemma set_cap_sets_direct:
  "P cap \<Longrightarrow> \<lbrace>\<top>\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace>" apply (rule hoare_strengthen_post) apply (rule set_cap_sets) apply (erule cte_wp_at_lift) by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P cap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. P cap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> set_cap cap slot \<lbrace>?Q\<rbrace>
 2. \<And>rv s. \<lbrakk>P cap; ?Q rv s\<rbrakk> \<Longrightarrow> cte_wp_at P slot s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>P cap; cte_wp_at (\<lambda>c. c = cap) slot s\<rbrakk> \<Longrightarrow> cte_wp_at P slot s proof (prove)
goal (1 subgoal):
 1. \<And>rv s sa. \<lbrakk>P cap; sa = cap\<rbrakk> \<Longrightarrow> P sa
theory Retype_AC

lemma delete_objects_pas_refined:
  "delete_objects ptr sz \<lbrace>pas_refined aag\<rbrace>" apply (simp add: delete_objects_def do_machine_op_def) apply (wp modify_wp | simp add: split_def)+ apply clarsimp apply (rule pas_refined_detype) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> delete_objects ptr sz \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> do y <- do ms <- gets machine_state;
(r, ms') <- select_f (freeMemory ptr sz ms);
modify (machine_state_update (\<lambda>_. ms'))
od;
modify (detype {ptr..ptr + 2 ^ sz - 1})
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<Longrightarrow> \<forall>x\<in>fst (freeMemory ptr sz (machine_state s)). pas_refined aag (detype {ptr..ptr + 2 ^ sz - 1} (s\<lparr>machine_state := snd x\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>pas_refined aag s; ((), b) \<in> fst (freeMemory ptr sz (machine_state s))\<rbrakk> \<Longrightarrow> pas_refined aag (detype {ptr..ptr + 2 ^ sz - 1} (s\<lparr>machine_state := b\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>pas_refined aag s; ((), b) \<in> fst (freeMemory ptr sz (machine_state s))\<rbrakk> \<Longrightarrow> pas_refined aag (s\<lparr>machine_state := b\<rparr>) proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma delete_objects_pspace_aligned[wp]:
  "delete_objects ptr sz \<lbrace>pspace_aligned\<rbrace>" unfolding delete_objects_def do_machine_op_def apply (wp | simp add: split_def detype_machine_state_update_comm)+ apply clarsimp apply (auto simp add: detype_def pspace_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> delete_objects ptr sz \<lbrace>\<lambda>_. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> do do ms <- gets machine_state;
(r, ms') <- select_f (freeMemory ptr sz ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od;
modify (detype {ptr..ptr + 2 ^ sz - 1})
od \<lbrace>\<lambda>_. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned s \<Longrightarrow> (\<exists>b. ((), b) \<in> fst (freeMemory ptr sz (machine_state s))) \<longrightarrow> pspace_aligned (detype {ptr..ptr + 2 ^ sz - 1} s) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>pspace_aligned s; ((), b) \<in> fst (freeMemory ptr sz (machine_state s))\<rbrakk> \<Longrightarrow> pspace_aligned (detype {ptr..ptr + 2 ^ sz - 1} s) proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma valid_vspace_objs_detype:
  assumes "invs s"
  assumes "cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s
                                           \<and> untyped_range c = {p..p + 2 ^ sz - 1}) ptr s"
  shows "valid_vspace_objs (detype {p..p + 2 ^ sz - 1} s)" proof - obtain c where c_def: "cte_wp_at ((=) c) ptr s \<and> is_untyped_cap c \<and> descendants_range c ptr s
                                                 \<and> untyped_range c = {p..p + 2 ^ sz - 1}" using assms by (fastforce dest: cte_wp_at_norm) have detype: "detype_locale_arch c ptr s" by unfold_locales (auto simp: assms c_def invs_untyped_children) thus ?thesis using detype_locale_arch.valid_vspace_obj_detype by (fastforce simp: c_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_objs (detype {p..p + 2 ^ sz - 1} s) proof (state)
goal (1 subgoal):
 1. valid_vspace_objs (detype {p..p + 2 ^ sz - 1} s) proof (prove)
goal (1 subgoal):
 1. (\<And>c. cte_wp_at ((=) c) ptr s \<and> is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {p..p + 2 ^ sz - 1} \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
invs s
cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {p..p + 2 ^ sz - 1}) ptr s

goal (1 subgoal):
 1. (\<And>c. cte_wp_at ((=) c) ptr s \<and> is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {p..p + 2 ^ sz - 1} \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
cte_wp_at ((=) c) ptr s \<and> is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {p..p + 2 ^ sz - 1}

goal (1 subgoal):
 1. valid_vspace_objs (detype {p..p + 2 ^ sz - 1} s) proof (prove)
goal (1 subgoal):
 1. detype_locale_arch c ptr s proof (state)
this:
detype_locale_arch c ptr s

goal (1 subgoal):
 1. valid_vspace_objs (detype {p..p + 2 ^ sz - 1} s) proof (prove)
using this:
detype_locale_arch c ptr s

goal (1 subgoal):
 1. valid_vspace_objs (detype {p..p + 2 ^ sz - 1} s) proof (prove)
using this:
detype_locale_arch c ptr s
detype_locale_arch ?cap ?ptr ?s \<Longrightarrow> valid_vspace_objs (detype (untyped_range ?cap) ?s)

goal (1 subgoal):
 1. valid_vspace_objs (detype {p..p + 2 ^ sz - 1} s) proof (state)
this:
valid_vspace_objs (detype {p..p + 2 ^ sz - 1} s)

goal:
No subgoals!
theory Retype_AC

lemma delete_objects_valid_vspace_objs:
  "\<lbrace>\<lambda>s. invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and>
                                        untyped_range c = {p..p + 2 ^ sz - 1}) ptr s)\<rbrace>
   delete_objects p sz
   \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" unfolding delete_objects_def do_machine_op_def apply (wp | simp add: split_def detype_machine_state_update_comm)+ apply (auto simp: valid_vspace_objs_detype) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {p..p + 2 ^ sz - 1}) ptr s)\<rbrace> delete_objects p sz \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {p..p + 2 ^ sz - 1}) ptr s)\<rbrace> do do ms <- gets machine_state;
(r, ms') <- select_f (freeMemory p sz ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od;
modify (detype {p..p + 2 ^ sz - 1})
od \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c (a, b) s \<and> untyped_range c = {p..p + 2 ^ sz - 1}) (a, b) s) \<Longrightarrow> (\<exists>b. ((), b) \<in> fst (freeMemory p sz (machine_state s))) \<longrightarrow> valid_vspace_objs (detype {p..p + 2 ^ sz - 1} s) proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma valid_arch_state_detype:
  assumes "invs s"
  assumes "cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s
                                           \<and> untyped_range c = {p..p + 2 ^ sz - 1}) ptr s"
  shows "valid_arch_state (detype {p..p + 2 ^ sz - 1} s)" proof - obtain c where c_def: "cte_wp_at ((=) c) ptr s \<and> is_untyped_cap c \<and> descendants_range c ptr s
                                                 \<and> untyped_range c = {p..p + 2 ^ sz - 1}" using assms by (fastforce dest: cte_wp_at_norm) have detype: "detype_locale_arch c ptr s" by unfold_locales (auto simp: assms c_def invs_untyped_children) thus ?thesis using detype_locale_arch.valid_arch_state_detype by (fastforce simp: c_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_state (detype {p..p + 2 ^ sz - 1} s) proof (state)
goal (1 subgoal):
 1. valid_arch_state (detype {p..p + 2 ^ sz - 1} s) proof (prove)
goal (1 subgoal):
 1. (\<And>c. cte_wp_at ((=) c) ptr s \<and> is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {p..p + 2 ^ sz - 1} \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
invs s
cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {p..p + 2 ^ sz - 1}) ptr s

goal (1 subgoal):
 1. (\<And>c. cte_wp_at ((=) c) ptr s \<and> is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {p..p + 2 ^ sz - 1} \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
cte_wp_at ((=) c) ptr s \<and> is_untyped_cap c \<and> descendants_range c ptr s \<and> untyped_range c = {p..p + 2 ^ sz - 1}

goal (1 subgoal):
 1. valid_arch_state (detype {p..p + 2 ^ sz - 1} s) proof (prove)
goal (1 subgoal):
 1. detype_locale_arch c ptr s proof (state)
this:
detype_locale_arch c ptr s

goal (1 subgoal):
 1. valid_arch_state (detype {p..p + 2 ^ sz - 1} s) proof (prove)
using this:
detype_locale_arch c ptr s

goal (1 subgoal):
 1. valid_arch_state (detype {p..p + 2 ^ sz - 1} s) proof (prove)
using this:
detype_locale_arch c ptr s
detype_locale_arch ?cap ?ptr ?s \<Longrightarrow> valid_arch_state (detype (untyped_range ?cap) ?s)

goal (1 subgoal):
 1. valid_arch_state (detype {p..p + 2 ^ sz - 1} s) proof (state)
this:
valid_arch_state (detype {p..p + 2 ^ sz - 1} s)

goal:
No subgoals!
theory Retype_AC

lemma data_to_obj_type_ret_not_asid_pool:
  "\<lbrace>\<top>\<rbrace> data_to_obj_type v \<lbrace>\<lambda>r s. r \<noteq> ArchObject ASIDPoolObj\<rbrace>, -" apply (clarsimp simp: validE_R_def validE_def valid_def) apply (auto simp: data_to_obj_type_def throwError_def returnOk_def
                    bindE_def return_def bind_def lift_def
             split: if_splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> data_to_obj_type v \<lbrace>\<lambda>r s. r \<noteq> ArchObject ASIDPoolObj\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s b. (Inr (ArchObject ASIDPoolObj), b) \<in> fst (data_to_obj_type v s) \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchRetype_AC

lemma invs_mdb_cte':
  "invs s \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s)" by (drule invs_mdb) (simp add: valid_mdb_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s)
theory ArchRetype_AC

lemma vs_refs_no_global_pts_default[simp]:
  "vs_refs_no_global_pts (default_object ty dev us) = {}" by (simp add: default_object_def default_arch_object_def tyunt
                vs_refs_no_global_pts_def pde_ref2_def pte_ref_def
                o_def
         split: apiobject_type.splits aobject_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_refs_no_global_pts (default_object ty dev us) = {}
theory ArchRetype_AC

lemma vrefs_eq: "state_vrefs s' = state_vrefs s" apply (rule ext) apply (simp add: s'_def state_vrefs_def ps_def orthr split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_vrefs s' = state_vrefs s proof (prove)
goal (1 subgoal):
 1. \<And>x. state_vrefs s' x = state_vrefs s x proof (prove)
goal:
No subgoals!