theory ArchDetype_AI

lemma valid_arch_state_detype[detype_invs_proofs]:
  "valid_arch_state (detype (untyped_range cap) s)" using valid_vs_lookup valid_arch_state ut_mdb valid_global_refsD [OF globals cap] cap apply (simp add: valid_arch_state_def valid_asid_table_def
                valid_global_pts_def global_refs_def
                cap_range_def) apply (clarsimp simp: ran_def arch_state_det) apply (drule vs_lookup_atI) apply (drule (1) valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI]) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (drule untyped_mdbD, rule untyped, assumption) apply blast apply assumption apply (drule descendants_range_inD[OF drange]) apply (simp add: cte_wp_at_caps_of_state) apply (simp add: cap_range_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_state (detype (untyped_range cap) s) proof (prove)
using this:
valid_vs_lookup s
valid_arch_state s
untyped_mdb (cdt s) (caps_of_state s)
?r \<in> global_refs s \<Longrightarrow> ?r \<notin> cap_range cap
cte_wp_at ((=) cap) ptr s

goal (1 subgoal):
 1. valid_arch_state (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vs_lookup s; (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> inj_on (asid_table s) (dom (asid_table s)) \<and> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s \<and> (\<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s) \<and> is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; cte_wp_at ((=) cap) ptr s\<rbrakk> \<Longrightarrow> (\<forall>p\<in>ran (asid_table (detype (untyped_range cap) s)). p \<notin> untyped_range cap \<and> typ_at (AArch AASIDPool) p s) \<and> inj_on (asid_table (detype (untyped_range cap) s)) (dom (asid_table (detype (untyped_range cap) s))) \<and> arm_global_pd (arch_state (detype (untyped_range cap) s)) \<notin> untyped_range cap \<and> typ_at (AArch APageDirectory) (arm_global_pd (arch_state (detype (untyped_range cap) s))) s \<and> (\<forall>p\<in>set (arm_global_pts (arch_state (detype (untyped_range cap) s))). p \<notin> untyped_range cap \<and> typ_at (AArch APageTable) p s) \<and> is_inv (arm_hwasid_table (arch_state (detype (untyped_range cap) s))) (map_option fst \<circ> arm_asid_map (arch_state (detype (untyped_range cap) s))) proof (prove)
goal (1 subgoal):
 1. \<And>p a. \<lbrakk>valid_vs_lookup s; untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; cte_wp_at ((=) cap) ptr s; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); asid_table s a = Some p; p \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p a. \<lbrakk>valid_vs_lookup s; untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; cte_wp_at ((=) cap) ptr s; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); p \<in> untyped_range cap; ([VSRef (UCAST(7 \<rightarrow> 32) a) None] \<rhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p a. \<lbrakk>valid_vs_lookup s; untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; cte_wp_at ((=) cap) ptr s; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); p \<in> untyped_range cap; \<exists>slot cap. caps_of_state s slot = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) a) None]\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p a aa b capa. \<lbrakk>valid_vs_lookup s; untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; caps_of_state s ptr = Some cap; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); p \<in> untyped_range cap; caps_of_state s (aa, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) a) None]\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>p a aa b capa. \<lbrakk>valid_vs_lookup s; untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); p \<in> untyped_range cap; caps_of_state s (aa, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) a) None]\<rbrakk> \<Longrightarrow> obj_refs capa \<inter> untyped_range cap \<noteq> {}
 2. \<And>p a aa b capa. \<lbrakk>valid_vs_lookup s; untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); p \<in> untyped_range cap; caps_of_state s (aa, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) a) None]\<rbrakk> \<Longrightarrow> untyped_mdb (?m29 p a aa b capa) (caps_of_state s)
 3. \<And>p a aa b capa. \<lbrakk>valid_vs_lookup s; untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); p \<in> untyped_range cap; caps_of_state s (aa, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) a) None]; (aa, b) \<in> descendants_of ptr (?m29 p a aa b capa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>p a aa b capa. \<lbrakk>valid_vs_lookup s; untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); p \<in> untyped_range cap; caps_of_state s (aa, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) a) None]\<rbrakk> \<Longrightarrow> untyped_mdb (?m29 p a aa b capa) (caps_of_state s)
 2. \<And>p a aa b capa. \<lbrakk>valid_vs_lookup s; untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); p \<in> untyped_range cap; caps_of_state s (aa, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) a) None]; (aa, b) \<in> descendants_of ptr (?m29 p a aa b capa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p a aa b capa. \<lbrakk>valid_vs_lookup s; untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); p \<in> untyped_range cap; caps_of_state s (aa, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) a) None]; (aa, b) \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>p a aa b capa. \<lbrakk>valid_vs_lookup s; untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); p \<in> untyped_range cap; caps_of_state s (aa, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) a) None]\<rbrakk> \<Longrightarrow> caps_of_state s (aa, b) = Some (?cap45 p a aa b capa)
 2. \<And>p a aa b capa. \<lbrakk>valid_vs_lookup s; untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); p \<in> untyped_range cap; caps_of_state s (aa, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) a) None]; cap_range (?cap45 p a aa b capa) \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p a aa b capa. \<lbrakk>valid_vs_lookup s; untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); p \<in> untyped_range cap; caps_of_state s (aa, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) a) None]; cap_range capa \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p a aa b capa. \<lbrakk>valid_vs_lookup s; untyped_mdb (cdt s) (caps_of_state s); \<And>r. r = idle_thread s \<or> r = arm_global_pd (arch_state s) \<or> r \<in> range (interrupt_irq_node s) \<or> r \<in> set (arm_global_pts (arch_state s)) \<Longrightarrow> r \<notin> untyped_range cap \<and> r \<notin> obj_refs cap; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); p \<in> untyped_range cap; caps_of_state s (aa, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) a) None]; (untyped_range capa \<union> obj_refs capa) \<inter> (untyped_range cap \<union> obj_refs cap) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!