theory ArchVSpace_AI

lemma vs_lookup_pages_pdeD:
  "([VSRef (vaddr >> 20) (Some APageDirectory),
     VSRef (asid && mask asid_low_bits) (Some AASIDPool),
     VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> p) s
   \<Longrightarrow>  \<exists>ap fun pd funa. ([VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> ap) s
               \<and> (arm_asid_table (arch_state s)) (asid_high_bits_of asid) = Some ap
               \<and> ko_at (ArchObj (ASIDPool fun)) ap s
               \<and> ([VSRef (asid && mask asid_low_bits) (Some AASIDPool),
                  VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pd) s
               \<and> fun (ucast (asid && mask asid_low_bits)) = Some pd
               \<and> ko_at (ArchObj (PageDirectory funa)) pd s
               \<and> pde_ref_pages (funa (ucast (vaddr >> 20))) = Some p" apply (frule vs_lookup_pages_2ConsD) apply clarsimp apply (frule_tac vs="[]" in vs_lookup_pages_2ConsD) apply clarsimp apply (rule_tac x=p'a in exI) apply (frule vs_lookup_atD[OF iffD2[OF fun_cong[OF vs_lookup_pages_eq_at]]]) apply (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def
                 dest!: graph_ofD
                 split: if_split_asm) apply (clarsimp split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits) apply (simp add: up_ucast_inj_eq graph_of_def kernel_mapping_slots_def kernel_base_def
                   not_le ucast_less_ucast_weak[symmetric, where 'a=12 and 'b=32]
                   mask_asid_low_bits_ucast_ucast pde_ref_pages_def
            split: if_split_asm) apply (simp add: ucast_ucast_id
            split: pde.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p) s \<Longrightarrow> \<exists>ap fun pd funa. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> ap) s \<and> asid_table s (asid_high_bits_of asid) = Some ap \<and> ako_at (ASIDPool fun) ap s \<and> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pd) s \<and> fun (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some pd \<and> ako_at (PageDirectory funa) pd s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p) s; \<exists>p'. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p') s \<and> (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'), [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> \<exists>ap fun pd funa. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> ap) s \<and> asid_table s (asid_high_bits_of asid) = Some ap \<and> ako_at (ASIDPool fun) ap s \<and> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pd) s \<and> fun (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some pd \<and> ako_at (PageDirectory funa) pd s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some p proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p) s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p') s; (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'), [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> \<exists>ap. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> ap) s \<and> asid_table s (asid_high_bits_of asid) = Some ap \<and> (\<exists>fun. ako_at (ASIDPool fun) ap s \<and> (\<exists>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pd) s \<and> fun (UCAST(32 \<rightarrow> 10) asid) = Some pd \<and> (\<exists>funa. ako_at (PageDirectory funa) pd s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some p))) proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p) s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p') s; (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'), [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<in> vs_lookup_pages1 s; \<exists>p'a. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s \<and> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'a), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p') \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> \<exists>ap. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> ap) s \<and> asid_table s (asid_high_bits_of asid) = Some ap \<and> (\<exists>fun. ako_at (ASIDPool fun) ap s \<and> (\<exists>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pd) s \<and> fun (UCAST(32 \<rightarrow> 10) asid) = Some pd \<and> (\<exists>funa. ako_at (PageDirectory funa) pd s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some p))) proof (prove)
goal (1 subgoal):
 1. \<And>p' p'a. \<lbrakk>([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p) s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p') s; (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'), [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<in> vs_lookup_pages1 s; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'a), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p') \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> \<exists>ap. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> ap) s \<and> asid_table s (asid_high_bits_of asid) = Some ap \<and> (\<exists>fun. ako_at (ASIDPool fun) ap s \<and> (\<exists>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pd) s \<and> fun (UCAST(32 \<rightarrow> 10) asid) = Some pd \<and> (\<exists>funa. ako_at (PageDirectory funa) pd s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some p))) proof (prove)
goal (1 subgoal):
 1. \<And>p' p'a. \<lbrakk>([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p) s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p') s; (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'), [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<in> vs_lookup_pages1 s; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'a), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p') \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s \<and> asid_table s (asid_high_bits_of asid) = Some p'a \<and> (\<exists>fun. ako_at (ASIDPool fun) p'a s \<and> (\<exists>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pd) s \<and> fun (UCAST(32 \<rightarrow> 10) asid) = Some pd \<and> (\<exists>funa. ako_at (PageDirectory funa) pd s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some p))) proof (prove)
goal (1 subgoal):
 1. \<And>p' p'a. \<lbrakk>([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p) s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p') s; (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'), [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<in> vs_lookup_pages1 s; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'a), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p') \<in> vs_lookup_pages1 s; asid_table s (asid_high_bits_of asid) = Some p'a\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s \<and> asid_table s (asid_high_bits_of asid) = Some p'a \<and> (\<exists>fun. ako_at (ASIDPool fun) p'a s \<and> (\<exists>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pd) s \<and> fun (UCAST(32 \<rightarrow> 10) asid) = Some pd \<and> (\<exists>funa. ako_at (PageDirectory funa) pd s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some p))) proof (prove)
goal (1 subgoal):
 1. \<And>p' p'a ko koa. \<lbrakk>([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p) s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p') s; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s; asid_table s (asid_high_bits_of asid) = Some p'a; kheap s p' = Some ko; (VSRef (vaddr >> 20) (Some APageDirectory), p) \<in> (case ko of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {}); kheap s p'a = Some koa; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), p') \<in> (case koa of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>fun. koa = ArchObj (ASIDPool fun) \<and> (\<exists>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pd) s \<and> fun (UCAST(32 \<rightarrow> 10) asid) = Some pd \<and> (\<exists>funa. kheap s pd = Some (ArchObj (PageDirectory funa)) \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some p)) proof (prove)
goal (1 subgoal):
 1. \<And>p'a x3 x1 a aa ba. \<lbrakk>([VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p) s; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> ba) s; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s; asid_table s (asid_high_bits_of asid) = Some p'a; kheap s ba = Some (ArchObj (PageDirectory x3)); kheap s p'a = Some (ArchObj (ASIDPool x1)); (a, p) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (x3 x)); (aa, ba) \<in> graph_of x1; vaddr >> 20 = UCAST(12 \<rightarrow> 32) a; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> \<exists>pd. ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pd) s \<and> x1 (UCAST(32 \<rightarrow> 10) asid) = Some pd \<and> (\<exists>funa. kheap s pd = Some (ArchObj (PageDirectory funa)) \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) a))) = Some p) proof (prove)
goal (1 subgoal):
 1. \<And>p'a x3 x1 a aa ba. \<lbrakk>x1 aa = Some ba; vaddr >> 20 = UCAST(12 \<rightarrow> 32) a; UCAST(32 \<rightarrow> 10) asid = aa; ([VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p) s; ([VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> ba) s; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s; asid_table s (asid_high_bits_of asid) = Some p'a; kheap s ba = Some (ArchObj (PageDirectory x3)); kheap s p'a = Some (ArchObj (ASIDPool x1)); UCAST(12 \<rightarrow> 32) a < 0xE00; (case x3 a of InvalidPDE \<Rightarrow> None | PageTablePDE ptr x z \<Rightarrow> Some (ptrFromPAddr ptr) | SectionPDE ptr x y z \<Rightarrow> Some (ptrFromPAddr ptr) | SuperSectionPDE ptr x z \<Rightarrow> Some (ptrFromPAddr ptr)) = Some p\<rbrakk> \<Longrightarrow> (case x3 (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) a)) of InvalidPDE \<Rightarrow> None | PageTablePDE ptr x z \<Rightarrow> Some (ptrFromPAddr ptr) | SectionPDE ptr x y z \<Rightarrow> Some (ptrFromPAddr ptr) | SuperSectionPDE ptr x z \<Rightarrow> Some (ptrFromPAddr ptr)) = Some p proof (prove)
goal:
No subgoals!