theory ArchVSpace_AI

lemma kernel_slot_impossible_vs_lookup_pages:
  "(ucast (vaddr >> 20)) \<in> kernel_mapping_slots \<Longrightarrow>
   \<not> ([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> pptr) s" apply (clarsimp simp: vs_lookup_pages_def vs_asid_refs_def
                 dest!: vs_lookup_pages1_rtrancl_iterations) apply (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def) apply (clarsimp simp: ucast_ucast_id
                 dest!: graph_ofD
                 split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits
                        if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 12) (vaddr >> 20) \<in> kernel_mapping_slots \<Longrightarrow> ([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], pptr) \<notin> vs_lookup_pages s proof (prove)
goal (1 subgoal):
 1. \<And>aa bd ae be af bf. \<lbrakk>UCAST(32 \<rightarrow> 12) (vaddr >> 20) \<in> kernel_mapping_slots; (aa, bd) \<in> graph_of (asid_table s); ((af, bf), [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], pptr) \<in> vs_lookup_pages1 s; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], bd), ae, be) \<in> vs_lookup_pages1 s; ((ae, be), af, bf) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>aa bd be bf ko koa kob. \<lbrakk>UCAST(32 \<rightarrow> 12) (vaddr >> 20) \<in> kernel_mapping_slots; (aa, bd) \<in> graph_of (asid_table s); kheap s bf = Some ko; kheap s bd = Some koa; kheap s be = Some kob; (VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<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> {}); (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), be) \<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> {}); (VSRef (vaddr >> 20) (Some APageDirectory), bf) \<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> {}); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!