theory ArchADT_AC

lemma ptable_state_objs_to_policy:
  "\<lbrakk> invs s; ptable_lift tcb s x = Some ptr;
     auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x);
     get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s);
     \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj))
                                     (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq>
                        Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings \<rbrakk>
     \<Longrightarrow> (get_pd_of_thread (kheap s) (arch_state s) tcb, auth, ptrFromPAddr ptr) \<in>
           state_objs_to_policy s" apply (simp add: state_objs_to_policy_def) apply (rule sbta_vref) apply (clarsimp simp: ptable_lift_def ptable_rights_def state_vrefs_def
                  split: option.splits) apply (frule pd_of_thread_page_directory_at, simp) apply (clarsimp simp: typ_at_eq_kheap_obj) apply (clarsimp simp: vs_refs_no_global_pts_def) apply (rule_tac x="(ucast (x >> 20), ptrFromPAddr a, aa,
                      vspace_cap_rights_to_auth b)" in bexI) apply clarsimp apply (rule_tac x="(ptrFromPAddr a + (x && mask aa), auth)" in image_eqI) apply (simp add: ptrFromPAddr_def) apply (simp add: ptr_offset_in_ptr_range) apply (simp add: kernel_mappings_kernel_mapping_slots') apply (clarsimp simp: graph_of_def) apply (clarsimp simp: get_page_info_def get_pd_entry_def pde_ref2_def
                  split: option.splits pde.splits arch_kernel_obj.splits) apply (clarsimp simp: get_arch_obj_def
                   split: option.splits kernel_object.splits arch_kernel_obj.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> (get_pd_of_thread (kheap s) (arch_state s) tcb, auth, ptrFromPAddr ptr) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> (get_pd_of_thread (kheap s) (arch_state s) tcb, auth, ptrFromPAddr ptr) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> (ptrFromPAddr ptr, ?uu, ?uv, auth) \<in> state_vrefs s (get_pd_of_thread (kheap s) (arch_state s) tcb) proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab b. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa)\<rbrakk> \<Longrightarrow> (\<exists>y. kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some y) \<and> (\<forall>x2. kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some x2 \<longrightarrow> (ptrFromPAddr (a + (x && mask aa)), ?uu, ?uv, auth) \<in> vs_refs_no_global_pts x2) proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab b. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); typ_at (AArch APageDirectory) (get_pd_of_thread (kheap s) (arch_state s) tcb) s\<rbrakk> \<Longrightarrow> (\<exists>y. kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some y) \<and> (\<forall>x2. kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some x2 \<longrightarrow> (ptrFromPAddr (a + (x && mask aa)), ?uu, ?uv, auth) \<in> vs_refs_no_global_pts x2) proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab b pd. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (ptrFromPAddr (a + (x && mask aa)), ?uu, ?uv, auth) \<in> vs_refs_no_global_pts (ArchObj (PageDirectory pd)) proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab b pd. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<exists>xa\<in>graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptrFromPAddr (a + (x && mask aa)), ?uu, ?uv, auth) \<in> (case xa 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 aa ab b pd. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (ptrFromPAddr (a + (x && mask aa)), ?uu, ?uv, auth) \<in> (case (UCAST(32 \<rightarrow> 12) (x >> 20), ptrFromPAddr a, aa, vspace_cap_rights_to_auth b) 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 aa ab b pd. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (x >> 20), ptrFromPAddr a, aa, vspace_cap_rights_to_auth b) \<in> graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x} proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab b pd. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (ptrFromPAddr (a + (x && mask aa)), ?uu, ?uv, auth) \<in> (\<lambda>xa. case xa of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (x >> 20)), APageDirectory, a)) ` (ptr_range (ptrFromPAddr a) aa \<times> vspace_cap_rights_to_auth b)
 2. \<And>a aa ab b pd. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (x >> 20), ptrFromPAddr a, aa, vspace_cap_rights_to_auth b) \<in> graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x} proof (prove)
goal (3 subgoals):
 1. \<And>a aa ab b pd. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (ptrFromPAddr (a + (x && mask aa)), ?uu, ?uv, auth) = (case (ptrFromPAddr a + (x && mask aa), auth) of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (x >> 20)), APageDirectory, a))
 2. \<And>a aa ab b pd. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (ptrFromPAddr a + (x && mask aa), auth) \<in> ptr_range (ptrFromPAddr a) aa \<times> vspace_cap_rights_to_auth b
 3. \<And>a aa ab b pd. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (x >> 20), ptrFromPAddr a, aa, vspace_cap_rights_to_auth b) \<in> graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x} proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab b pd. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (ptrFromPAddr a + (x && mask aa), auth) \<in> ptr_range (ptrFromPAddr a) aa \<times> vspace_cap_rights_to_auth b
 2. \<And>a aa ab b pd. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (x >> 20), ptrFromPAddr a, aa, vspace_cap_rights_to_auth b) \<in> graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x} proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab b pd. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (x >> 20), ptrFromPAddr a, aa, vspace_cap_rights_to_auth b) \<in> graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x} proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab b pd. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (x >> 20), ptrFromPAddr a, aa, vspace_cap_rights_to_auth b) \<in> graph_of (pde_ref2 \<circ> pd) proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab b pd. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> pde_ref2 (pd (UCAST(32 \<rightarrow> 12) (x >> 20))) = Some (ptrFromPAddr a, aa, vspace_cap_rights_to_auth b) proof (prove)
goal (2 subgoals):
 1. \<And>a ab b pd x33 x3. \<lbrakk>ptr = a + (x && mask 20); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd)); auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_arch_obj (Some (ArchObj (PageDirectory pd))) = Some (PageDirectory x3); x \<notin> kernel_mappings; invs s; x3 (UCAST(32 \<rightarrow> 12) (x >> 20)) = SectionPDE a ab x33 b\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (x >> 20)) \<noteq> InvalidPDE \<and> (\<forall>x21 x22 x23. pd (UCAST(32 \<rightarrow> 12) (x >> 20)) \<noteq> PageTablePDE x21 x22 x23) \<and> (\<forall>x31 x32 x33 x34. pd (UCAST(32 \<rightarrow> 12) (x >> 20)) = SectionPDE x31 x32 x33 x34 \<longrightarrow> ptrFromPAddr x31 = ptrFromPAddr a \<and> vspace_cap_rights_to_auth x34 = vspace_cap_rights_to_auth b) \<and> (\<forall>x41 x42 x43. pd (UCAST(32 \<rightarrow> 12) (x >> 20)) \<noteq> SuperSectionPDE x41 x42 x43)
 2. \<And>a ab b pd x3. \<lbrakk>ptr = a + (x && mask 24); kheap s (get_pd_of_thread (kheap s) (arch_state s) tcb) = Some (ArchObj (PageDirectory pd)); auth \<in> vspace_cap_rights_to_auth b; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_arch_obj (Some (ArchObj (PageDirectory pd))) = Some (PageDirectory x3); x \<notin> kernel_mappings; invs s; x3 (UCAST(32 \<rightarrow> 12) (x >> 20)) = SuperSectionPDE a ab b\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (x >> 20)) \<noteq> InvalidPDE \<and> (\<forall>x21 x22 x23. pd (UCAST(32 \<rightarrow> 12) (x >> 20)) \<noteq> PageTablePDE x21 x22 x23) \<and> (\<forall>x31 x32 x33 x34. pd (UCAST(32 \<rightarrow> 12) (x >> 20)) \<noteq> SectionPDE x31 x32 x33 x34) \<and> (\<forall>x41 x42 x43. pd (UCAST(32 \<rightarrow> 12) (x >> 20)) = SuperSectionPDE x41 x42 x43 \<longrightarrow> ptrFromPAddr x41 = ptrFromPAddr a \<and> vspace_cap_rights_to_auth x43 = vspace_cap_rights_to_auth b) proof (prove)
goal:
No subgoals!