theory ArchVSpace_AI

lemma vs_lookup_pages_pteD:
  "([VSRef ((vaddr >> 12) && mask 8) (Some APageTable),
     VSRef (vaddr >> 20) (Some APageDirectory),
     VSRef (asid && mask asid_low_bits) (Some AASIDPool),
     VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pg) s
   \<Longrightarrow>  \<exists>ap fun pd funa pt funb. ([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> ([VSRef (vaddr >> 20) (Some APageDirectory),
                  VSRef (asid && mask asid_low_bits) (Some AASIDPool),
                  VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pt) s
               \<and> pde_ref_pages (funa (ucast (vaddr >> 20))) = Some pt
               \<and> ko_at (ArchObj (PageTable funb)) pt s
               \<and> pte_ref_pages (funb (ucast ((vaddr >> 12) && mask 8 ))) = Some pg" apply (frule vs_lookup_pages_2ConsD) apply clarsimp apply (frule_tac vs="[z]" for z in vs_lookup_pages_2ConsD) apply clarsimp apply (frule_tac vs="[]" in vs_lookup_pages_2ConsD) apply clarsimp apply (rule_tac x=p'b 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 pte_ref_pages_def
            split: if_split_asm) apply (simp add: ucast_ucast_id
            split: pde.split_asm pte.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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> pg) s \<Longrightarrow> \<exists>ap fun pd funa pt funb. ([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> ([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> pt) s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some pt \<and> ako_at (PageTable funb) pt s \<and> pte_ref_pages (funb (UCAST(32 \<rightarrow> 8) ((vaddr >> 12) && mask 8))) = Some pg proof (prove)
goal (1 subgoal):
 1. \<lbrakk>([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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> pg) s; \<exists>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] \<unrhd> p') s \<and> (([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'), [VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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], pg) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> \<exists>ap fun pd funa pt funb. ([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> ([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> pt) s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some pt \<and> ako_at (PageTable funb) pt s \<and> pte_ref_pages (funb (UCAST(32 \<rightarrow> 8) ((vaddr >> 12) && mask 8))) = Some pg proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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> pg) s; ([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 (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'), [VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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], pg) \<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> (\<exists>pt. ([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> pt) s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some pt \<and> (\<exists>funb. ako_at (PageTable funb) pt s \<and> pte_ref_pages (funb (UCAST(32 \<rightarrow> 8) ((vaddr >> 12) && mask 8))) = Some pg))))) proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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> pg) s; ([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 (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'), [VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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], pg) \<in> vs_lookup_pages1 s; \<exists>p'a. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s \<and> (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'a), [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> (\<exists>pt. ([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> pt) s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some pt \<and> (\<exists>funb. ako_at (PageTable funb) pt s \<and> pte_ref_pages (funb (UCAST(32 \<rightarrow> 8) ((vaddr >> 12) && mask 8))) = Some pg))))) proof (prove)
goal (1 subgoal):
 1. \<And>p' p'a. \<lbrakk>([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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> pg) s; ([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 (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'), [VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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], pg) \<in> vs_lookup_pages1 s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s; (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'a), [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> (\<exists>pt. ([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> pt) s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some pt \<and> (\<exists>funb. ako_at (PageTable funb) pt s \<and> pte_ref_pages (funb (UCAST(32 \<rightarrow> 8) ((vaddr >> 12) && mask 8))) = Some pg))))) proof (prove)
goal (1 subgoal):
 1. \<And>p' p'a. \<lbrakk>([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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> pg) s; ([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 (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'), [VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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], pg) \<in> vs_lookup_pages1 s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s; (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'a), [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'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p') s \<and> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'a) \<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> (\<exists>pt. ([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> pt) s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some pt \<and> (\<exists>funb. ako_at (PageTable funb) pt s \<and> pte_ref_pages (funb (UCAST(32 \<rightarrow> 8) ((vaddr >> 12) && mask 8))) = Some pg))))) proof (prove)
goal (1 subgoal):
 1. \<And>p' p'a p'b. \<lbrakk>([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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> pg) s; ([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 (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'), [VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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], pg) \<in> vs_lookup_pages1 s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s; (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'a), [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'b) s; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'b), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'a) \<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> (\<exists>pt. ([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> pt) s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some pt \<and> (\<exists>funb. ako_at (PageTable funb) pt s \<and> pte_ref_pages (funb (UCAST(32 \<rightarrow> 8) ((vaddr >> 12) && mask 8))) = Some pg))))) proof (prove)
goal (1 subgoal):
 1. \<And>p' p'a p'b. \<lbrakk>([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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> pg) s; ([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 (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'), [VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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], pg) \<in> vs_lookup_pages1 s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s; (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'a), [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'b) s; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'b), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'a) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'b) s \<and> asid_table s (asid_high_bits_of asid) = Some p'b \<and> (\<exists>fun. ako_at (ASIDPool fun) p'b 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> (\<exists>pt. ([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> pt) s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some pt \<and> (\<exists>funb. ako_at (PageTable funb) pt s \<and> pte_ref_pages (funb (UCAST(32 \<rightarrow> 8) ((vaddr >> 12) && mask 8))) = Some pg))))) proof (prove)
goal (1 subgoal):
 1. \<And>p' p'a p'b. \<lbrakk>([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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> pg) s; ([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 (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'), [VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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], pg) \<in> vs_lookup_pages1 s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'a) s; (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'a), [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'b) s; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'b), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'a) \<in> vs_lookup_pages1 s; asid_table s (asid_high_bits_of asid) = Some p'b\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'b) s \<and> asid_table s (asid_high_bits_of asid) = Some p'b \<and> (\<exists>fun. ako_at (ASIDPool fun) p'b 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> (\<exists>pt. ([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> pt) s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some pt \<and> (\<exists>funb. ako_at (PageTable funb) pt s \<and> pte_ref_pages (funb (UCAST(32 \<rightarrow> 8) ((vaddr >> 12) && mask 8))) = Some pg))))) proof (prove)
goal (1 subgoal):
 1. \<And>p' p'a p'b ko koa kob. \<lbrakk>([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 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> pg) s; ([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'a) s; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'b) s; asid_table s (asid_high_bits_of asid) = Some p'b; kheap s p' = Some ko; (VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pg) \<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 (vaddr >> 20) (Some APageDirectory), 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> {}); kheap s p'b = Some kob; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), p'a) \<in> (case kob 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. kob = 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> (\<exists>pt. ([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> pt) s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (vaddr >> 20))) = Some pt \<and> (\<exists>funb. kheap s pt = Some (ArchObj (PageTable funb)) \<and> pte_ref_pages (funb (UCAST(32 \<rightarrow> 8) ((vaddr >> 12) && mask 8))) = Some pg)))) proof (prove)
goal (1 subgoal):
 1. \<And>p'b x2 x3 x1 a aa ba ab bb. \<lbrakk>([VSRef (UCAST(8 \<rightarrow> 32) a) (Some APageTable), VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ab) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pg) s; ([VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ab) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> ba) s; ([VSRef (UCAST(10 \<rightarrow> 32) ab) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> bb) s; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'b) s; asid_table s (asid_high_bits_of asid) = Some p'b; kheap s ba = Some (ArchObj (PageTable x2)); kheap s bb = Some (ArchObj (PageDirectory x3)); kheap s p'b = Some (ArchObj (ASIDPool x1)); (a, pg) \<in> graph_of (pte_ref_pages \<circ> x2); (aa, ba) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (x3 x)); (ab, bb) \<in> graph_of x1; (vaddr >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) a; vaddr >> 20 = UCAST(12 \<rightarrow> 32) aa; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> \<exists>pd. ([VSRef (UCAST(10 \<rightarrow> 32) ab) (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> (\<exists>pt. ([VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ab) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pt) s \<and> pde_ref_pages (funa (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) aa))) = Some pt \<and> (\<exists>funb. kheap s pt = Some (ArchObj (PageTable funb)) \<and> pte_ref_pages (funb (UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) a))) = Some pg))) proof (prove)
goal (1 subgoal):
 1. \<And>p'b x2 x3 x1 a aa ba ab bb. \<lbrakk>x1 ab = Some bb; (vaddr >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) a; vaddr >> 20 = UCAST(12 \<rightarrow> 32) aa; UCAST(32 \<rightarrow> 10) asid = ab; ([VSRef (UCAST(8 \<rightarrow> 32) a) (Some APageTable), VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ab) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pg) s; ([VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ab) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> ba) s; ([VSRef (UCAST(10 \<rightarrow> 32) ab) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> bb) s; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p'b) s; asid_table s (asid_high_bits_of asid) = Some p'b; kheap s ba = Some (ArchObj (PageTable x2)); kheap s bb = Some (ArchObj (PageDirectory x3)); kheap s p'b = Some (ArchObj (ASIDPool x1)); (case x2 a of InvalidPTE \<Rightarrow> None | LargePagePTE ptr x z \<Rightarrow> Some (ptrFromPAddr ptr) | SmallPagePTE ptr x z \<Rightarrow> Some (ptrFromPAddr ptr)) = Some pg; UCAST(12 \<rightarrow> 32) aa < 0xE00; (case x3 aa 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 ba\<rbrakk> \<Longrightarrow> \<exists>pt. ([VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), VSRef (UCAST(10 \<rightarrow> 32) ab) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pt) s \<and> (case x3 (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) aa)) 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 pt \<and> (\<exists>funb. kheap s pt = Some (ArchObj (PageTable funb)) \<and> (case funb (UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) a)) of InvalidPTE \<Rightarrow> None | LargePagePTE ptr x z \<Rightarrow> Some (ptrFromPAddr ptr) | SmallPagePTE ptr x z \<Rightarrow> Some (ptrFromPAddr ptr)) = Some pg) proof (prove)
goal:
No subgoals!