theory ArchAcc_AI

lemma store_pde_invs_unmap:
  "\<lbrace>invs and valid_pde pde and (\<lambda>s. wellformed_pde pde)
            and K (ucast (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots)
            and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s)
            and K (pde = InvalidPDE)\<rbrace>
  store_pde p pde \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: store_pde_def del: split_paired_Ex) apply (wp set_pd_invs_unmap) apply (clarsimp simp del: split_paired_Ex del: exE) apply (rule conjI) apply (drule invs_valid_objs) apply (fastforce simp: valid_objs_def dom_def obj_at_def valid_obj_def) apply (rule conjI) apply clarsimp apply (drule (1) valid_vspace_objsD, fastforce) apply simp apply (rule conjI) apply (clarsimp intro!: pair_imageI
                   simp: obj_at_def vs_refs_def vs_refs_pages_def map_conv_upd graph_of_def pde_ref_def pde_ref_pages_def
                   split: if_split_asm)+ apply (clarsimp simp: empty_table_def) apply (cases pde, (auto simp: pde_ref_def  valid_pde_mappings_def split:if_split_asm)) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_pde pde and (\<lambda>s. wellformed_pde pde) and K (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s) and K (pde = InvalidPDE)\<rbrace> store_pde p pde \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_pde pde and (\<lambda>s. wellformed_pde pde) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s) and (\<lambda>y. pde = InvalidPDE)\<rbrace> do pd <- get_pd (p && ~~ mask pd_bits);
set_pd (p && ~~ mask pd_bits) (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and valid_pde pde and (\<lambda>s. wellformed_pde pde) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s) and (\<lambda>y. pde = InvalidPDE)) s \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (invs and (\<lambda>s. \<forall>i. wellformed_pde ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) i)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> valid_vspace_obj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))) s) and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) \<subseteq> vs_refs_pages ko) (p && ~~ mask pd_bits) and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x = pd' x)) (p && ~~ mask pd_bits) and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s) and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))))) s proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (\<forall>i. i \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> wellformed_pde (pd i)) \<and> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s)) \<and> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs_pages ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> InvalidPDE = pd' (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> pd x = pd' x))) (p && ~~ mask pd_bits) s \<and> (obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> \<forall>i. i \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> wellformed_pde (pd i)
 2. \<And>s pd. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s)) \<and> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs_pages ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> InvalidPDE = pd' (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> pd x = pd' x))) (p && ~~ mask pd_bits) s \<and> (obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s; valid_objs s\<rbrakk> \<Longrightarrow> \<forall>i. i \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> wellformed_pde (pd i)
 2. \<And>s pd. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s)) \<and> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs_pages ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> InvalidPDE = pd' (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> pd x = pd' x))) (p && ~~ mask pd_bits) s \<and> (obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s)) \<and> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs_pages ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> InvalidPDE = pd' (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> pd x = pd' x))) (p && ~~ mask pd_bits) s \<and> (obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) s)
 2. \<And>s pd. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs_pages ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> InvalidPDE = pd' (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> pd x = pd' x))) (p && ~~ mask pd_bits) s \<and> (obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pd x ref. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s; x \<notin> kernel_mapping_slots; (ref \<rhd> (p && ~~ mask pd_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> valid_pde (pd x) s
 2. \<And>s pd. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs_pages ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> InvalidPDE = pd' (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> pd x = pd' x))) (p && ~~ mask pd_bits) s \<and> (obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pd x ref. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s; x \<notin> kernel_mapping_slots; x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); valid_vspace_obj (PageDirectory pd) s\<rbrakk> \<Longrightarrow> valid_pde (pd x) s
 2. \<And>s pd. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs_pages ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> InvalidPDE = pd' (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> pd x = pd' x))) (p && ~~ mask pd_bits) s \<and> (obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs_pages ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> InvalidPDE = pd' (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> pd x = pd' x))) (p && ~~ mask pd_bits) s \<and> (obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs_pages ko) (p && ~~ mask pd_bits) s
 2. \<And>s pd. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)))) \<subseteq> vs_refs ko) (p && ~~ mask pd_bits) s \<and> obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> InvalidPDE = pd' (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> pd x = pd' x))) (p && ~~ mask pd_bits) s \<and> (obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)) x)) = Some y} \<subseteq> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) = Some y} \<and> (empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>invs s; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p && ~~ mask pd_bits \<notin> global_refs s; pde = InvalidPDE; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := InvalidPDE)) x)) = Some y} \<subseteq> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) = Some y} \<and> ((\<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE)) \<longrightarrow> (\<forall>r. pde_ref InvalidPDE = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings InvalidPDE) proof (prove)
goal:
No subgoals!