theory Dpolicy

lemma state_vrefs_transform_rev:
  "\<lbrakk> einvs s; opt_cap ptr (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap;
     auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap \<rbrakk> \<Longrightarrow>
     \<exists>ref aat. (ptr', ref, aat, auth) \<in> state_vrefs s (fst ptr)" apply (case_tac ptr, clarsimp) apply (subgoal_tac "a \<noteq> idle_thread s") prefer 2 apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def
                        opt_cap_def slots_of_def) apply (clarsimp simp: map_add_def object_slots_def) apply (case_tac "kheap s a") apply (clarsimp simp: state_vrefs_def transform_def transform_objects_def
                         opt_cap_def slots_of_def) apply (clarsimp simp: map_add_def object_slots_def) apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def
                       opt_cap_def slots_of_def) apply (case_tac aa, simp_all add: transform_object_def object_slots_def nat_split_conv_to_if
                             split: if_split_asm) apply (clarsimp simp:transform_cnode_contents_def is_real_cap_transform) apply (clarsimp simp:transform_cnode_contents_def is_real_cap_transform) apply (frule valid_etcbs_tcb_etcb [rotated], fastforce) apply (clarsimp simp: transform_tcb_def is_real_cap_transform is_real_cap_infer_tcb_pending_op
                         is_real_cap_infer_tcb_bound_notification
                   split:if_split_asm) apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj, simp_all add:vs_refs_no_global_pts_def graph_of_def) apply (clarsimp simp:transform_asid_pool_contents_def unat_map_def split:if_split_asm) apply (rule exI) apply (rename_tac "fun") apply (case_tac "fun (of_nat b)") apply (clarsimp simp:transform_asid_pool_entry_def) apply (fastforce simp:transform_asid_pool_entry_def cdl_cap_auth_conferred_def) apply (clarsimp simp:transform_asid_pool_entry_def) apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:if_split_asm) apply (rule exI)+ apply (drule pte_ref_transform_rev) apply safe[1] apply simp apply (rule_tac x="(ptr', auth)" in image_eqI) apply simp apply simp apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:if_split_asm) apply (subgoal_tac "(of_nat b :: 12 word) < ucast (kernel_base >> 20)") prefer 2 apply (subst word_not_le[symmetric]) apply (rule notI) apply (clarsimp simp:kernel_pde_mask_def transform_pde_def) apply (simp add:kernel_pde_mask_def not_less[symmetric]) apply (rule exI) apply (drule pde_ref_transform_rev, clarsimp) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> state_vrefs s (fst ptr) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> state_vrefs s a proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> state_vrefs s a
 2. \<And>a b. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s
 2. \<And>a b. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> state_vrefs s a proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>(case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) (idle_thread s) of None \<Rightarrow> \<lambda>x. None | Some x2 \<Rightarrow> object_slots x2) b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (idle_thread s, b); invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> state_vrefs s a proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> state_vrefs s a proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = None\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> state_vrefs s a
 2. \<And>a b aa. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some aa\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> state_vrefs s a proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) a of None \<Rightarrow> \<lambda>x. None | Some x2 \<Rightarrow> object_slots x2) b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = None\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some aa\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> state_vrefs s a proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>opt_cap (a, b) (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some aa\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> state_vrefs s a proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>object_slots (transform_object (machine_state s) a (ekheap s a) aa) b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some aa\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts aa proof (prove)
goal (4 subgoals):
 1. \<And>a b aa x11 x12. \<lbrakk>ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode 0 x12); aa = kernel_object.CNode 0 x12; x11 = 0; transform_cnode_contents 0 x12 b = Some cap\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts (kernel_object.CNode 0 x12)
 2. \<And>a b aa x11 x12. \<lbrakk>ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); aa = kernel_object.CNode x11 x12; 0 < x11; transform_cnode_contents x11 x12 b = Some cap\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts (kernel_object.CNode x11 x12)
 3. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts (TCB x2)
 4. \<And>a b aa x5. \<lbrakk>(case case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr> of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); aa = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts (ArchObj x5) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa x11 x12. \<lbrakk>ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); aa = kernel_object.CNode x11 x12; 0 < x11; transform_cnode_contents x11 x12 b = Some cap\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts (kernel_object.CNode x11 x12)
 2. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts (TCB x2)
 3. \<And>a b aa x5. \<lbrakk>(case case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr> of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); aa = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts (ArchObj x5) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts (TCB x2)
 2. \<And>a b aa x5. \<lbrakk>(case case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr> of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); aa = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts (ArchObj x5) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); aa = TCB x2; \<exists>etcb. ekheap s a = Some etcb\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts (TCB x2)
 2. \<And>a b aa x5. \<lbrakk>(case case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr> of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); aa = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts (ArchObj x5) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa x5. \<lbrakk>(case case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr> of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); aa = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts (ArchObj x5) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa arch_kernel_obj. \<lbrakk>(case case arch_kernel_obj of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr> of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj arch_kernel_obj); aa = ArchObj arch_kernel_obj\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts (ArchObj arch_kernel_obj) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa arch_kernel_obj x1. \<lbrakk>transform_asid_pool_contents x1 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (ASIDPool x1)); aa = ArchObj (ASIDPool x1); arch_kernel_obj = ASIDPool x1\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` {(x, y). x1 x = Some y}
 2. \<And>a b aa arch_kernel_obj x2. \<lbrakk>transform_page_table_contents x2 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); aa = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> \<exists>ref aat a aa ab b. pte_ref (x2 a) = Some (aa, ab, b) \<and> (ptr', ref, aat, auth) \<in> (\<lambda>x. case x of (p, aa) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) a, APageTable, aa)) ` (ptr_range aa ab \<times> b)
 3. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (3 subgoals):
 1. \<And>a b x1. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_asid_pool_entry (x1 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_asid_pool_entry (x1 (word_of_nat b))); \<not> is_real_cap (transform_asid_pool_entry (x1 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (ASIDPool x1)); b < 1024; cap = transform_asid_pool_entry (x1 (word_of_nat b))\<rbrakk> \<Longrightarrow> \<exists>ref aat. (ptr', ref, aat, auth) \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` {(x, y). x1 x = Some y}
 2. \<And>a b aa arch_kernel_obj x2. \<lbrakk>transform_page_table_contents x2 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); aa = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> \<exists>ref aat a aa ab b. pte_ref (x2 a) = Some (aa, ab, b) \<and> (ptr', ref, aat, auth) \<in> (\<lambda>x. case x of (p, aa) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) a, APageTable, aa)) ` (ptr_range aa ab \<times> b)
 3. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (3 subgoals):
 1. \<And>a b x1. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_asid_pool_entry (x1 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_asid_pool_entry (x1 (word_of_nat b))); \<not> is_real_cap (transform_asid_pool_entry (x1 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (ASIDPool x1)); b < 1024; cap = transform_asid_pool_entry (x1 (word_of_nat b))\<rbrakk> \<Longrightarrow> \<exists>aat. (ptr', ?ref173 a b x1, aat, auth) \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` {(x, y). x1 x = Some y}
 2. \<And>a b aa arch_kernel_obj x2. \<lbrakk>transform_page_table_contents x2 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); aa = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> \<exists>ref aat a aa ab b. pte_ref (x2 a) = Some (aa, ab, b) \<and> (ptr', ref, aat, auth) \<in> (\<lambda>x. case x of (p, aa) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) a, APageTable, aa)) ` (ptr_range aa ab \<times> b)
 3. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (3 subgoals):
 1. \<And>a b fun. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_asid_pool_entry (fun (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_asid_pool_entry (fun (word_of_nat b))); \<not> is_real_cap (transform_asid_pool_entry (fun (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (ASIDPool fun)); b < 1024; cap = transform_asid_pool_entry (fun (word_of_nat b))\<rbrakk> \<Longrightarrow> \<exists>aat. (ptr', ?ref173 a b fun, aat, auth) \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` {(x, y). fun x = Some y}
 2. \<And>a b aa arch_kernel_obj x2. \<lbrakk>transform_page_table_contents x2 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); aa = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> \<exists>ref aat a aa ab b. pte_ref (x2 a) = Some (aa, ab, b) \<and> (ptr', ref, aat, auth) \<in> (\<lambda>x. case x of (p, aa) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) a, APageTable, aa)) ` (ptr_range aa ab \<times> b)
 3. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (4 subgoals):
 1. \<And>a b fun. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_asid_pool_entry (fun (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_asid_pool_entry (fun (word_of_nat b))); \<not> is_real_cap (transform_asid_pool_entry (fun (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (ASIDPool fun)); b < 1024; cap = transform_asid_pool_entry (fun (word_of_nat b)); fun (word_of_nat b) = None\<rbrakk> \<Longrightarrow> \<exists>aat. (ptr', ?ref173 a b fun, aat, auth) \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` {(x, y). fun x = Some y}
 2. \<And>a b fun aa. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_asid_pool_entry (fun (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_asid_pool_entry (fun (word_of_nat b))); \<not> is_real_cap (transform_asid_pool_entry (fun (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (ASIDPool fun)); b < 1024; cap = transform_asid_pool_entry (fun (word_of_nat b)); fun (word_of_nat b) = Some aa\<rbrakk> \<Longrightarrow> \<exists>aat. (ptr', ?ref173 a b fun, aat, auth) \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` {(x, y). fun x = Some y}
 3. \<And>a b aa arch_kernel_obj x2. \<lbrakk>transform_page_table_contents x2 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); aa = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> \<exists>ref aat a aa ab b. pte_ref (x2 a) = Some (aa, ab, b) \<and> (ptr', ref, aat, auth) \<in> (\<lambda>x. case x of (p, aa) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) a, APageTable, aa)) ` (ptr_range aa ab \<times> b)
 4. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (3 subgoals):
 1. \<And>a b fun aa. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_asid_pool_entry (fun (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_asid_pool_entry (fun (word_of_nat b))); \<not> is_real_cap (transform_asid_pool_entry (fun (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (ASIDPool fun)); b < 1024; cap = transform_asid_pool_entry (fun (word_of_nat b)); fun (word_of_nat b) = Some aa\<rbrakk> \<Longrightarrow> \<exists>aat. (ptr', ?ref173 a b fun, aat, auth) \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` {(x, y). fun x = Some y}
 2. \<And>a b aa arch_kernel_obj x2. \<lbrakk>transform_page_table_contents x2 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); aa = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> \<exists>ref aat a aa ab b. pte_ref (x2 a) = Some (aa, ab, b) \<and> (ptr', ref, aat, auth) \<in> (\<lambda>x. case x of (p, aa) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) a, APageTable, aa)) ` (ptr_range aa ab \<times> b)
 3. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa arch_kernel_obj x2. \<lbrakk>transform_page_table_contents x2 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); aa = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> \<exists>ref aat a aa ab b. pte_ref (x2 a) = Some (aa, ab, b) \<and> (ptr', ref, aat, auth) \<in> (\<lambda>x. case x of (p, aa) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) a, APageTable, aa)) ` (ptr_range aa ab \<times> b)
 2. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (2 subgoals):
 1. \<And>a b x2. \<lbrakk>transform_page_table_contents x2 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2))\<rbrakk> \<Longrightarrow> \<exists>ref aat a aa ab b. pte_ref (x2 a) = Some (aa, ab, b) \<and> (ptr', ref, aat, auth) \<in> (\<lambda>x. case x of (p, aa) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) a, APageTable, aa)) ` (ptr_range aa ab \<times> b)
 2. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (2 subgoals):
 1. \<And>a b x2. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pte (x2 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b))); \<not> is_real_cap (transform_pte (x2 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); b < 256; cap = transform_pte (x2 (word_of_nat b))\<rbrakk> \<Longrightarrow> \<exists>ref aat a aa ab b. pte_ref (x2 a) = Some (aa, ab, b) \<and> (ptr', ref, aat, auth) \<in> (\<lambda>x. case x of (p, aa) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) a, APageTable, aa)) ` (ptr_range aa ab \<times> b)
 2. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (2 subgoals):
 1. \<And>a b x2. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pte (x2 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b))); \<not> is_real_cap (transform_pte (x2 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); b < 256; cap = transform_pte (x2 (word_of_nat b))\<rbrakk> \<Longrightarrow> pte_ref (x2 (?a208 a b x2)) = Some (?a210 a b x2, ?a212 a b x2, ?b214 a b x2) \<and> (ptr', ?ref204 a b x2, ?aat206 a b x2, auth) \<in> (\<lambda>x. case x of (p, aa) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) (?a208 a b x2), APageTable, aa)) ` (ptr_range (?a210 a b x2) (?a212 a b x2) \<times> ?b214 a b x2)
 2. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (2 subgoals):
 1. \<And>a b x2. \<lbrakk>auth \<in> cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b))); \<not> is_real_cap (transform_pte (x2 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); b < 256; cap = transform_pte (x2 (word_of_nat b)); pte_ref (x2 (word_of_nat b)) = Some (cap_object (transform_pte (x2 (word_of_nat b))), get_size (transform_pte (x2 (word_of_nat b))), cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b)))) \<and> ptr' \<in> ptr_range (cap_object (transform_pte (x2 (word_of_nat b)))) (get_size (transform_pte (x2 (word_of_nat b))))\<rbrakk> \<Longrightarrow> pte_ref (x2 (?a208 a b x2)) = Some (?a210 a b x2, ?a212 a b x2, ?b214 a b x2) \<and> (ptr', ?ref204 a b x2, ?aat206 a b x2, auth) \<in> (\<lambda>x. case x of (p, aa) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) (?a208 a b x2), APageTable, aa)) ` (ptr_range (?a210 a b x2) (?a212 a b x2) \<times> ?b214 a b x2)
 2. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (3 subgoals):
 1. \<And>a b x2. \<lbrakk>auth \<in> cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b))); \<not> is_real_cap (transform_pte (x2 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); b < 256; cap = transform_pte (x2 (word_of_nat b)); pte_ref (x2 (word_of_nat b)) = Some (cap_object (transform_pte (x2 (word_of_nat b))), get_size (transform_pte (x2 (word_of_nat b))), cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b)))); ptr' \<in> ptr_range (cap_object (transform_pte (x2 (word_of_nat b)))) (get_size (transform_pte (x2 (word_of_nat b))))\<rbrakk> \<Longrightarrow> pte_ref (x2 (?a208 a b x2)) = Some (?a210 a b x2, ?a212 a b x2, ?b214 a b x2)
 2. \<And>a b x2. \<lbrakk>auth \<in> cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b))); \<not> is_real_cap (transform_pte (x2 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); b < 256; cap = transform_pte (x2 (word_of_nat b)); pte_ref (x2 (word_of_nat b)) = Some (cap_object (transform_pte (x2 (word_of_nat b))), get_size (transform_pte (x2 (word_of_nat b))), cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b)))); ptr' \<in> ptr_range (cap_object (transform_pte (x2 (word_of_nat b)))) (get_size (transform_pte (x2 (word_of_nat b))))\<rbrakk> \<Longrightarrow> (ptr', ?ref204 a b x2, ?aat206 a b x2, auth) \<in> (\<lambda>x. case x of (p, aa) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) (?a208 a b x2), APageTable, aa)) ` (ptr_range (?a210 a b x2) (?a212 a b x2) \<times> ?b214 a b x2)
 3. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (2 subgoals):
 1. \<And>a b x2. \<lbrakk>auth \<in> cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b))); \<not> is_real_cap (transform_pte (x2 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); b < 256; cap = transform_pte (x2 (word_of_nat b)); pte_ref (x2 (word_of_nat b)) = Some (cap_object (transform_pte (x2 (word_of_nat b))), get_size (transform_pte (x2 (word_of_nat b))), cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b)))); ptr' \<in> ptr_range (cap_object (transform_pte (x2 (word_of_nat b)))) (get_size (transform_pte (x2 (word_of_nat b))))\<rbrakk> \<Longrightarrow> (ptr', ?ref204 a b x2, ?aat206 a b x2, auth) \<in> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) (word_of_nat b), APageTable, a)) ` (ptr_range (cap_object (transform_pte (x2 (word_of_nat b)))) (get_size (transform_pte (x2 (word_of_nat b)))) \<times> cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b))))
 2. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (3 subgoals):
 1. \<And>a b x2. \<lbrakk>auth \<in> cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b))); \<not> is_real_cap (transform_pte (x2 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); b < 256; cap = transform_pte (x2 (word_of_nat b)); pte_ref (x2 (word_of_nat b)) = Some (cap_object (transform_pte (x2 (word_of_nat b))), get_size (transform_pte (x2 (word_of_nat b))), cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b)))); ptr' \<in> ptr_range (cap_object (transform_pte (x2 (word_of_nat b)))) (get_size (transform_pte (x2 (word_of_nat b))))\<rbrakk> \<Longrightarrow> (ptr', ?ref204 a b x2, ?aat206 a b x2, auth) = (case (ptr', auth) of (p, a) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) (word_of_nat b), APageTable, a))
 2. \<And>a b x2. \<lbrakk>auth \<in> cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b))); \<not> is_real_cap (transform_pte (x2 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); b < 256; cap = transform_pte (x2 (word_of_nat b)); pte_ref (x2 (word_of_nat b)) = Some (cap_object (transform_pte (x2 (word_of_nat b))), get_size (transform_pte (x2 (word_of_nat b))), cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b)))); ptr' \<in> ptr_range (cap_object (transform_pte (x2 (word_of_nat b)))) (get_size (transform_pte (x2 (word_of_nat b))))\<rbrakk> \<Longrightarrow> (ptr', auth) \<in> ptr_range (cap_object (transform_pte (x2 (word_of_nat b)))) (get_size (transform_pte (x2 (word_of_nat b)))) \<times> cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b)))
 3. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (2 subgoals):
 1. \<And>a b x2. \<lbrakk>auth \<in> cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b))); \<not> is_real_cap (transform_pte (x2 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); b < 256; cap = transform_pte (x2 (word_of_nat b)); pte_ref (x2 (word_of_nat b)) = Some (cap_object (transform_pte (x2 (word_of_nat b))), get_size (transform_pte (x2 (word_of_nat b))), cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b)))); ptr' \<in> ptr_range (cap_object (transform_pte (x2 (word_of_nat b)))) (get_size (transform_pte (x2 (word_of_nat b))))\<rbrakk> \<Longrightarrow> (ptr', auth) \<in> ptr_range (cap_object (transform_pte (x2 (word_of_nat b)))) (get_size (transform_pte (x2 (word_of_nat b)))) \<times> cdl_cap_auth_conferred (transform_pte (x2 (word_of_nat b)))
 2. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; ptr' \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (1 subgoal):
 1. \<And>a b x3. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde (kernel_pde_mask x3 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_pde (kernel_pde_mask x3 (word_of_nat b))); \<not> is_real_cap (transform_pde (kernel_pde_mask x3 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); b < 4096; cap = transform_pde (kernel_pde_mask x3 (word_of_nat b))\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (2 subgoals):
 1. \<And>a b x3. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde (kernel_pde_mask x3 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_pde (kernel_pde_mask x3 (word_of_nat b))); \<not> is_real_cap (transform_pde (kernel_pde_mask x3 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); b < 4096; cap = transform_pde (kernel_pde_mask x3 (word_of_nat b)); word_of_nat b < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth))
 2. \<And>a b x3. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde (kernel_pde_mask x3 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_pde (kernel_pde_mask x3 (word_of_nat b))); \<not> is_real_cap (transform_pde (kernel_pde_mask x3 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); b < 4096; cap = transform_pde (kernel_pde_mask x3 (word_of_nat b))\<rbrakk> \<Longrightarrow> word_of_nat b < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) proof (prove)
goal (2 subgoals):
 1. \<And>a b x3. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde (kernel_pde_mask x3 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_pde (kernel_pde_mask x3 (word_of_nat b))); \<not> is_real_cap (transform_pde (kernel_pde_mask x3 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); b < 4096; cap = transform_pde (kernel_pde_mask x3 (word_of_nat b))\<rbrakk> \<Longrightarrow> word_of_nat b < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)
 2. \<And>a b x3. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde (kernel_pde_mask x3 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_pde (kernel_pde_mask x3 (word_of_nat b))); \<not> is_real_cap (transform_pde (kernel_pde_mask x3 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); b < 4096; cap = transform_pde (kernel_pde_mask x3 (word_of_nat b)); word_of_nat b < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (2 subgoals):
 1. \<And>a b x3. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde (kernel_pde_mask x3 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_pde (kernel_pde_mask x3 (word_of_nat b))); \<not> is_real_cap (transform_pde (kernel_pde_mask x3 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); b < 4096; cap = transform_pde (kernel_pde_mask x3 (word_of_nat b))\<rbrakk> \<Longrightarrow> \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> word_of_nat b
 2. \<And>a b x3. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde (kernel_pde_mask x3 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_pde (kernel_pde_mask x3 (word_of_nat b))); \<not> is_real_cap (transform_pde (kernel_pde_mask x3 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); b < 4096; cap = transform_pde (kernel_pde_mask x3 (word_of_nat b)); word_of_nat b < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (2 subgoals):
 1. \<And>a b x3. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde (kernel_pde_mask x3 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_pde (kernel_pde_mask x3 (word_of_nat b))); \<not> is_real_cap (transform_pde (kernel_pde_mask x3 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); b < 4096; cap = transform_pde (kernel_pde_mask x3 (word_of_nat b)); UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> word_of_nat b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b x3. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde (kernel_pde_mask x3 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_pde (kernel_pde_mask x3 (word_of_nat b))); \<not> is_real_cap (transform_pde (kernel_pde_mask x3 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); b < 4096; cap = transform_pde (kernel_pde_mask x3 (word_of_nat b)); word_of_nat b < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (1 subgoal):
 1. \<And>a b x3. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde (kernel_pde_mask x3 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_pde (kernel_pde_mask x3 (word_of_nat b))); \<not> is_real_cap (transform_pde (kernel_pde_mask x3 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); b < 4096; cap = transform_pde (kernel_pde_mask x3 (word_of_nat b)); word_of_nat b < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (1 subgoal):
 1. \<And>a b x3. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde (x3 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_pde (x3 (word_of_nat b))); \<not> is_real_cap (transform_pde (x3 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); b < 4096; cap = transform_pde (x3 (word_of_nat b)); word_of_nat b < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)\<rbrakk> \<Longrightarrow> \<exists>ref aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). \<not> x < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)}. (ptr', ref, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (1 subgoal):
 1. \<And>a b x3. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde (x3 (word_of_nat b))); auth \<in> cdl_cap_auth_conferred (transform_pde (x3 (word_of_nat b))); \<not> is_real_cap (transform_pde (x3 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); b < 4096; cap = transform_pde (x3 (word_of_nat b)); word_of_nat b < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)\<rbrakk> \<Longrightarrow> \<exists>aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). \<not> x < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)}. (ptr', ?ref248 a b x3, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (1 subgoal):
 1. \<And>a b x3. \<lbrakk>auth \<in> cdl_cap_auth_conferred (transform_pde (x3 (word_of_nat b))); \<not> is_real_cap (transform_pde (x3 (word_of_nat b))); ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); b < 4096; cap = transform_pde (x3 (word_of_nat b)); word_of_nat b < UCAST(32 \<rightarrow> 12) (kernel_base >> 20); pde_ref2 (x3 (word_of_nat b)) = Some (cap_object (transform_pde (x3 (word_of_nat b))), get_size (transform_pde (x3 (word_of_nat b))), cdl_cap_auth_conferred (transform_pde (x3 (word_of_nat b)))); ptr' \<in> ptr_range (cap_object (transform_pde (x3 (word_of_nat b)))) (get_size (transform_pde (x3 (word_of_nat b))))\<rbrakk> \<Longrightarrow> \<exists>aat. \<exists>x\<in>{(x, y). pde_ref2 (x3 x) = Some y} - {(x, y). \<not> x < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)}. (ptr', ?ref248 a b x3, aat, auth) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal:
No subgoals!