theory ArchVSpace_AI

lemma kernel_slot_impossible_vs_lookup_pages2:
  "(ucast (vaddr >> 20)) \<in> kernel_mapping_slots \<Longrightarrow>
   \<not> ([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 >> 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 b ab bb. \<lbrakk>UCAST(32 \<rightarrow> 12) (vaddr >> 20) \<in> kernel_mapping_slots; (aa, b) \<in> graph_of (asid_table s); (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], b), ab, bb) \<in> vs_lookup_pages1 s; ((ab, bb), [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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>aa b bb ko koa. \<lbrakk>UCAST(32 \<rightarrow> 12) (vaddr >> 20) \<in> kernel_mapping_slots; (aa, b) \<in> graph_of (asid_table s); kheap s b = Some ko; kheap s bb = Some koa; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb) \<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 (vaddr >> 20) (Some APageDirectory), pptr) \<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> {}); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!