kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchDetype_AI

lemma valid_vspace_obj:
  "\<And>ao p. \<lbrakk> valid_vspace_obj ao s; ko_at (ArchObj ao) p s; (\<exists>\<rhd>p) s \<rbrakk> \<Longrightarrow>
       valid_vspace_obj ao (detype (untyped_range cap) s)" apply (case_tac ao; simp; erule allEI ballEI; clarsimp simp: ran_def;
         drule vs_lookup_pages_vs_lookupI) subgoal for p t r ref i by (crush i) subgoal for p t i ref by (cases "t i"; crush i) subgoal for p t i ref by (cases "t i"; crush i) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ao p. \<lbrakk>valid_vspace_obj ao s; ako_at ao p s; \<exists>ref. (ref \<rhd> p) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (detype (untyped_range cap) s) proof (prove)
goal (3 subgoals):
 1. \<And>p x1 x ref a. \<lbrakk>ako_at (ASIDPool x1) p s; typ_at (AArch APageDirectory) x s; x1 a = Some x; x \<in> untyped_range cap; (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> False
 2. \<And>p x2 x ref. \<lbrakk>ako_at (PageTable x2) p s; valid_pte (x2 x) s; (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> valid_pte (x2 x) (detype (untyped_range cap) s)
 3. \<And>p x3 x ref. \<lbrakk>ako_at (PageDirectory x3) p s; x \<notin> kernel_mapping_slots; valid_pde (x3 x) s; (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> valid_pde (x3 x) (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ako_at (ASIDPool t) p s; typ_at (AArch APageDirectory) r s; t i = Some r; r \<in> untyped_range cap; (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>p x2 x ref. \<lbrakk>ako_at (PageTable x2) p s; valid_pte (x2 x) s; (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> valid_pte (x2 x) (detype (untyped_range cap) s)
 2. \<And>p x3 x ref. \<lbrakk>ako_at (PageDirectory x3) p s; x \<notin> kernel_mapping_slots; valid_pde (x3 x) s; (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> valid_pde (x3 x) (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ako_at (PageTable t) p s; valid_pte (t i) s; (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> valid_pte (t i) (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<And>p x3 x ref. \<lbrakk>ako_at (PageDirectory x3) p s; x \<notin> kernel_mapping_slots; valid_pde (x3 x) s; (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> valid_pde (x3 x) (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ako_at (PageDirectory t) p s; i \<notin> kernel_mapping_slots; valid_pde (t i) s; (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> valid_pde (t i) (detype (untyped_range cap) s) proof (prove)
goal:
No subgoals!
theory ArchDetype_AI

lemma valid_vspace_obj_detype[detype_invs_proofs]: "valid_vspace_objs (detype (untyped_range cap) s)" proof - have "valid_vspace_objs s" using invs by fastforce thus ?thesis unfolding valid_vspace_objs_def apply (simp add: vs_lookup) apply (auto intro: valid_vspace_obj) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_objs (detype (untyped_range cap) s) proof (state)
goal (1 subgoal):
 1. valid_vspace_objs (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. valid_vspace_objs s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. valid_vspace_objs s proof (state)
this:
valid_vspace_objs s

goal (1 subgoal):
 1. valid_vspace_objs (detype (untyped_range cap) s) proof (prove)
using this:
valid_vspace_objs s

goal (1 subgoal):
 1. valid_vspace_objs (detype (untyped_range cap) s) proof (prove)
using this:
\<forall>p rs ao. (rs \<rhd> p) s \<longrightarrow> ako_at ao p s \<longrightarrow> valid_vspace_obj ao s

goal (1 subgoal):
 1. \<forall>p rs ao. (rs \<rhd> p) (detype (untyped_range cap) s) \<longrightarrow> ako_at ao p (detype (untyped_range cap) s) \<longrightarrow> valid_vspace_obj ao (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s) \<Longrightarrow> \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. p \<notin> untyped_range cap \<and> ako_at ao p s \<longrightarrow> valid_vspace_obj ao (detype (untyped_range cap) s)) proof (prove)
goal:
No subgoals! proof (state)
this:
valid_vspace_objs (detype (untyped_range cap) s)

goal:
No subgoals!
theory ArchDetype_AI

lemma unique_table_caps:
    "\<And>cps P. unique_table_caps cps
             \<Longrightarrow> unique_table_caps (\<lambda>x. if P x then None else cps x)" by (simp add: unique_table_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>cps P. unique_table_caps cps \<Longrightarrow> unique_table_caps (\<lambda>x. if P x then None else cps x)
theory ArchDetype_AI

lemma valid_table_caps:
  "valid_table_caps s \<Longrightarrow> valid_table_caps (detype (untyped_range cap) s)" apply (simp add: valid_table_caps_def del: imp_disjL) apply (elim allEI | rule impI)+ apply clarsimp apply (metis detype_arch_state no_obj_refs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_table_caps s \<Longrightarrow> valid_table_caps (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s \<Longrightarrow> \<forall>r a. a \<notin> untyped_range cap \<longrightarrow> (\<forall>b capa. caps_of_state s (a, b) = Some capa \<longrightarrow> is_pd_cap capa \<or> is_pt_cap capa \<longrightarrow> cap_asid capa = None \<longrightarrow> r \<in> obj_refs capa \<longrightarrow> r \<notin> untyped_range cap \<and> obj_at (empty_table (set (second_level_tables (arch_state (detype (untyped_range cap) s))))) r s) proof (prove)
goal (1 subgoal):
 1. \<And>r a b capa. \<lbrakk>a \<notin> untyped_range cap; caps_of_state s (a, b) = Some capa \<longrightarrow> is_pd_cap capa \<or> is_pt_cap capa \<longrightarrow> cap_asid capa = None \<longrightarrow> r \<in> obj_refs capa \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s (a, b) = Some capa; is_pd_cap capa \<or> is_pt_cap capa; cap_asid capa = None; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> r \<notin> untyped_range cap \<and> obj_at (empty_table (set (second_level_tables (arch_state (detype (untyped_range cap) s))))) r s proof (prove)
goal (1 subgoal):
 1. \<And>r a b capa. \<lbrakk>a \<notin> untyped_range cap; obj_at (empty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s (a, b) = Some capa; is_pd_cap capa \<or> is_pt_cap capa; cap_asid capa = None; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> r \<notin> untyped_range cap \<and> obj_at (empty_table (set (second_level_tables (arch_state (detype (untyped_range cap) s))))) r s proof (prove)
goal:
No subgoals!
theory ArchDetype_AI

lemma unique_table_refs:
    "\<And>cps P. unique_table_refs cps
             \<Longrightarrow> unique_table_refs (\<lambda>x. if P x then None else cps x)" apply (simp only: unique_table_refs_def option.simps
                      simp_thms
               split: if_split) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>cps P. unique_table_refs cps \<Longrightarrow> unique_table_refs (\<lambda>x. if P x then None else cps x) proof (prove)
goal (1 subgoal):
 1. \<And>cps P. \<forall>p p' cap cap'. cps p = Some cap \<longrightarrow> cps p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap \<Longrightarrow> \<forall>p. \<not> P p \<longrightarrow> (\<forall>p'. \<not> P p' \<longrightarrow> (\<forall>cap cap'. cps p = Some cap \<longrightarrow> cps p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap)) proof (prove)
goal:
No subgoals!
theory ArchDetype_AI

lemma valid_arch_caps_detype[detype_invs_proofs]: "valid_arch_caps (detype (untyped_range cap) s)" using valid_arch_caps by (simp add: valid_arch_caps_def
                                       unique_table_caps
                                       valid_vs_lookup'
                                       unique_table_refs
                                       valid_table_caps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_caps (detype (untyped_range cap) s) proof (prove)
using this:
valid_arch_caps s

goal (1 subgoal):
 1. valid_arch_caps (detype (untyped_range cap) s)
theory ArchDetype_AI

lemma pd_at_global_pd: "page_directory_at (arm_global_pd (arch_state s)) s" using valid_arch_state by (simp add: valid_arch_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s proof (prove)
using this:
valid_arch_state s

goal (1 subgoal):
 1. typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s
theory ArchDetype_AI

lemma valid_kernel_mappings_detype[detype_invs_proofs]: "valid_kernel_mappings (detype (untyped_range cap) s)" proof - have "valid_kernel_mappings s" using invs by (simp add: invs_def valid_state_def) thus ?thesis by (simp add: valid_kernel_mappings_def detype_def
                  ball_ran_eq) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_kernel_mappings (detype (untyped_range cap) s) proof (state)
goal (1 subgoal):
 1. valid_kernel_mappings (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. valid_kernel_mappings s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. valid_kernel_mappings s proof (state)
this:
valid_kernel_mappings s

goal (1 subgoal):
 1. valid_kernel_mappings (detype (untyped_range cap) s) proof (prove)
using this:
valid_kernel_mappings s

goal (1 subgoal):
 1. valid_kernel_mappings (detype (untyped_range cap) s) proof (state)
this:
valid_kernel_mappings (detype (untyped_range cap) s)

goal:
No subgoals!
theory ArchDetype_AI

lemma valid_asid_map_detype[detype_invs_proofs]: "valid_asid_map (detype (untyped_range cap) s)" proof - have "valid_asid_map s" using invs by (simp add: invs_def valid_state_def) thus ?thesis apply (clarsimp simp: valid_asid_map_def arch_state_det) apply (drule bspec) apply (blast) apply (clarsimp simp: vspace_at_asid_def vs_lookup) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_asid_map (detype (untyped_range cap) s) proof (state)
goal (1 subgoal):
 1. valid_asid_map (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. valid_asid_map s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. valid_asid_map s proof (state)
this:
valid_asid_map s

goal (1 subgoal):
 1. valid_asid_map (detype (untyped_range cap) s) proof (prove)
using this:
valid_asid_map s

goal (1 subgoal):
 1. valid_asid_map (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> vspace_at_asid a b (detype (untyped_range cap) s) \<and> a \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}\<rbrakk> \<Longrightarrow> ?x9 a aa b \<in> graph_of (arm_asid_map (arch_state s))
 2. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; case ?x9 a aa b of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> vspace_at_asid a b (detype (untyped_range cap) s) \<and> a \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; case (a, aa, b) of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> vspace_at_asid a b (detype (untyped_range cap) s) \<and> a \<noteq> 0 proof (prove)
goal:
No subgoals! proof (state)
this:
valid_asid_map (detype (untyped_range cap) s)

goal:
No subgoals!
theory ArchDetype_AI

lemma equal_kernel_mappings_detype[detype_invs_proofs]:
  "equal_kernel_mappings (detype (untyped_range cap) s)" proof - have "equal_kernel_mappings s" using invs by (simp add: invs_def valid_state_def) thus ?thesis apply (simp add: equal_kernel_mappings_def) apply blast done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equal_kernel_mappings (detype (untyped_range cap) s) proof (state)
goal (1 subgoal):
 1. equal_kernel_mappings (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. equal_kernel_mappings s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. equal_kernel_mappings s proof (state)
this:
equal_kernel_mappings s

goal (1 subgoal):
 1. equal_kernel_mappings (detype (untyped_range cap) s) proof (prove)
using this:
equal_kernel_mappings s

goal (1 subgoal):
 1. equal_kernel_mappings (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<forall>x y pd pd'. ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w) \<Longrightarrow> \<forall>x y pd pd'. x \<notin> untyped_range cap \<and> ako_at (PageDirectory pd) x s \<and> y \<notin> untyped_range cap \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w) proof (prove)
goal:
No subgoals! proof (state)
this:
equal_kernel_mappings (detype (untyped_range cap) s)

goal:
No subgoals!
theory ArchDetype_AI

lemma valid_global_mappings_detype[detype_invs_proofs]:
  "valid_global_vspace_mappings (detype (untyped_range cap) s)" proof - have "valid_global_vspace_mappings s" using invs by (simp add: invs_def valid_state_def) thus ?thesis using valid_global_refsD [OF globals cap] valid_global_objs apply - apply (erule valid_global_vspace_mappings_pres, simp_all) apply (simp add: cap_range_def global_refs_def arch_state_det)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_vspace_mappings (detype (untyped_range cap) s) proof (state)
goal (1 subgoal):
 1. valid_global_vspace_mappings (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. valid_global_vspace_mappings s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. valid_global_vspace_mappings s proof (state)
this:
valid_global_vspace_mappings s

goal (1 subgoal):
 1. valid_global_vspace_mappings (detype (untyped_range cap) s) proof (prove)
using this:
valid_global_vspace_mappings s

goal (1 subgoal):
 1. valid_global_vspace_mappings (detype (untyped_range cap) s) proof (prove)
using this:
valid_global_vspace_mappings s
?r \<in> global_refs s \<Longrightarrow> ?r \<notin> cap_range cap
valid_global_objs s

goal (1 subgoal):
 1. valid_global_vspace_mappings (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_global_vspace_mappings s; \<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; valid_global_objs s\<rbrakk> \<Longrightarrow> valid_global_vspace_mappings (detype (untyped_range cap) s) proof (prove)
goal (4 subgoals):
 1. \<And>pd. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; valid_global_objs s; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<notin> untyped_range cap
 2. \<And>pt p. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; valid_global_objs s; ako_at (PageTable pt) p s; p \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> p \<notin> untyped_range cap
 3. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; valid_global_objs s\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state (detype (untyped_range cap) s)) = arm_global_pd (arch_state s)
 4. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; valid_global_objs s\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state (detype (untyped_range cap) s)) = arm_kernel_vspace (arch_state s) proof (prove)
goal:
No subgoals! proof (state)
this:
valid_global_vspace_mappings (detype (untyped_range cap) s)

goal:
No subgoals!
theory ArchDetype_AI

lemma pspace_in_kernel_window_detype[detype_invs_proofs]:
  "pspace_in_kernel_window (detype (untyped_range cap) s)" proof - have "pspace_in_kernel_window s" using invs by (simp add: invs_def valid_state_def) thus ?thesis apply (simp add: pspace_in_kernel_window_def arch_state_det) apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_in_kernel_window (detype (untyped_range cap) s) proof (state)
goal (1 subgoal):
 1. pspace_in_kernel_window (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. pspace_in_kernel_window s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. pspace_in_kernel_window s proof (state)
this:
pspace_in_kernel_window s

goal (1 subgoal):
 1. pspace_in_kernel_window (detype (untyped_range cap) s) proof (prove)
using this:
pspace_in_kernel_window s

goal (1 subgoal):
 1. pspace_in_kernel_window (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<forall>x ko. kheap s x = Some ko \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ obj_bits ko - 1}. arm_kernel_vspace (arch_state s) y = ArmVSpaceKernelWindow) \<Longrightarrow> \<forall>x ko. kheap s x = Some ko \<and> x \<notin> untyped_range cap \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ obj_bits ko - 1}. arm_kernel_vspace (arch_state s) y = ArmVSpaceKernelWindow) proof (prove)
goal:
No subgoals! proof (state)
this:
pspace_in_kernel_window (detype (untyped_range cap) s)

goal:
No subgoals!
theory ArchDetype_AI

lemma cap_refs_respects_device_region_detype[detype_invs_proofs]:
  "cap_refs_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s))" proof - have "cap_refs_respects_device_region s" using invs by (simp add: invs_def valid_state_def) thus ?thesis apply (clarsimp simp: clear_um_def cap_refs_respects_device_region_def
                simp del: split_paired_All split_paired_Ex) apply (drule_tac x = "(a,b)" in spec) apply (clarsimp simp: cte_wp_at_caps_of_state cap_range_respects_device_region_def detype_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_refs_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (state)
goal (1 subgoal):
 1. cap_refs_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (prove)
goal (1 subgoal):
 1. cap_refs_respects_device_region s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. cap_refs_respects_device_region s proof (state)
this:
cap_refs_respects_device_region s

goal (1 subgoal):
 1. cap_refs_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (prove)
using this:
cap_refs_respects_device_region s

goal (1 subgoal):
 1. cap_refs_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>cref. \<not> cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s) cref s; cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c (detype (untyped_range cap) s)) (a, b) s\<rbrakk> \<Longrightarrow> a \<in> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c (detype (untyped_range cap) s)) (a, b) s; \<not> cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s) (a, b) s\<rbrakk> \<Longrightarrow> a \<in> untyped_range cap proof (prove)
goal:
No subgoals! proof (state)
this:
cap_refs_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s))

goal:
No subgoals!
theory ArchDetype_AI

lemma valid_machine_state_detype[detype_invs_proofs]:
    "valid_machine_state (clear_um (untyped_range cap) (detype (untyped_range cap) s))" proof - have "valid_machine_state s" using invs by (simp add: invs_def valid_state_def) thus ?thesis using untyped cap_is_valid by (clarsimp simp: valid_machine_state_def clear_um_def
      detype_def in_user_frame_eq in_device_frame_eq) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_machine_state (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (state)
goal (1 subgoal):
 1. valid_machine_state (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (prove)
goal (1 subgoal):
 1. valid_machine_state s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. valid_machine_state s proof (state)
this:
valid_machine_state s

goal (1 subgoal):
 1. valid_machine_state (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (prove)
using this:
valid_machine_state s

goal (1 subgoal):
 1. valid_machine_state (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (prove)
using this:
valid_machine_state s
is_untyped_cap cap
s \<turnstile> cap

goal (1 subgoal):
 1. valid_machine_state (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (state)
this:
valid_machine_state (clear_um (untyped_range cap) (detype (untyped_range cap) s))

goal:
No subgoals!
theory Untyped_AI

lemma valid_untyped_inv_wcap:
  "valid_untyped_inv ui
    = (\<lambda>s. \<exists>sz idx. valid_untyped_inv_wcap ui (Some
        (case ui of Retype slot reset ptr_base ptr ty us slots dev
            \<Rightarrow> UntypedCap dev (ptr && ~~ mask sz) sz idx)) s)" apply (cases ui) apply (clarsimp simp: fun_eq_iff cte_wp_at_caps_of_state
    intro!: arg_cong[where f=Ex] conj_cong[OF refl]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_untyped_inv ui = (\<lambda>s. \<exists>sz idx. valid_untyped_inv_wcap ui (Some (case ui of Retype slot reset ptr_base ptr ty us slots dev \<Rightarrow> UntypedCap dev (ptr && ~~ mask sz) sz idx)) s) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8. ui = Retype x1 x2 x3 x4 x5 x6 x7 x8 \<Longrightarrow> valid_untyped_inv ui = (\<lambda>s. \<exists>sz idx. valid_untyped_inv_wcap ui (Some (case ui of Retype slot reset ptr_base ptr ty us slots dev \<Rightarrow> UntypedCap dev (ptr && ~~ mask sz) sz idx)) s) proof (prove)
goal (1 subgoal):
 1. \<And>a b x2 x3 x4 x5 x6 x7 x8 x xa xb. \<lbrakk>ui = Retype (a, b) x2 x3 x4 x5 x6 x7 x8; caps_of_state x (a, b) = Some (UntypedCap x8 x3 xa xb)\<rbrakk> \<Longrightarrow> (range_cover x4 xa (obj_bits_api x5 x6) (length x7) \<and> (xb \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask xa = x3 \<and> (x2 \<longrightarrow> descendants_of (a, b) (cdt x) = {}) \<and> (x5 = CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6) \<and> (a, b) \<notin> set x7 \<and> distinct x7 \<and> (\<forall>slot\<in>set x7. caps_of_state x slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot x \<and> real_cte_at slot x) \<and> x5 \<noteq> ArchObject ASIDPoolObj \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5)) = (x4 && ~~ mask xa = x3 \<and> range_cover x4 xa (obj_bits_api x5 x6) (length x7) \<and> (xb \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask xa = x3 \<and> (x2 \<longrightarrow> descendants_of (a, b) (cdt x) = {}) \<and> (x5 = CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6) \<and> (a, b) \<notin> set x7 \<and> distinct x7 \<and> (\<forall>slot\<in>set x7. caps_of_state x slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot x \<and> real_cte_at slot x) \<and> x5 \<noteq> ArchObject ASIDPoolObj \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5)) proof (prove)
goal:
No subgoals!