theory ArchADT_AC

lemma pd_of_thread_page_directory_at:
  "\<lbrakk> invs s; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s) \<rbrakk>
     \<Longrightarrow> page_directory_at ((get_pd_of_thread (kheap s) (arch_state s) tcb)) s" apply (clarsimp simp: get_pd_of_thread_def
                 split: option.splits kernel_object.splits cap.splits arch_cap.splits if_splits) apply (frule_tac t=tcb in objs_valid_tcb_vtable[OF invs_valid_objs]) apply (simp add: get_tcb_def) apply (fastforce simp: valid_cap_def2 valid_cap_ref_def valid_arch_cap_ref_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) (get_pd_of_thread (kheap s) (arch_state s) tcb) s proof (prove)
goal (1 subgoal):
 1. \<And>x2a x51 x2b x2c x5 x51a x52a x2e. \<lbrakk>invs s; kheap s tcb = Some (TCB x2a); tcb_vtable x2a = ArchObjectCap (PageDirectoryCap x51 (Some x2b)); asid_table s (asid_high_bits_of x2b) = Some x2c; kheap s x2c = Some (ArchObj x5); (VSRef (x2b && mask local.asid_low_bits) (Some AASIDPool), x51) \<in> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | 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 (pd x)) | _ \<Rightarrow> {}); x51 \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> (asid_table s (asid_high_bits_of x2e) = None \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x2. (kheap s x2 = None \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x2a. (\<forall>x11 x12. x2a = CNode x11 x12 \<longrightarrow> kheap s x2 = Some (CNode x11 x12) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x2c. x2a = TCB x2c \<longrightarrow> kheap s x2 = Some (TCB x2c) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x3. x2a = Endpoint x3 \<longrightarrow> kheap s x2 = Some (Endpoint x3) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x4. x2a = Notification x4 \<longrightarrow> kheap s x2 = Some (Notification x4) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x5. ((VSRef (x2e && mask local.asid_low_bits) (Some AASIDPool), x51a) \<in> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | 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 (pd x)) | _ \<Rightarrow> {}) \<longrightarrow> x2a = ArchObj x5 \<longrightarrow> kheap s x2 = Some (ArchObj x5) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) x51a s) \<and> ((VSRef (x2e && mask local.asid_low_bits) (Some AASIDPool), x51a) \<notin> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | 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 (pd x)) | _ \<Rightarrow> {}) \<longrightarrow> x2a = ArchObj x5 \<longrightarrow> kheap s x2 = Some (ArchObj x5) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s)))) proof (prove)
goal (2 subgoals):
 1. \<And>x2a x51 x2b x2c x5 x51a x52a x2e. \<lbrakk>invs s; kheap s tcb = Some (TCB x2a); tcb_vtable x2a = ArchObjectCap (PageDirectoryCap x51 (Some x2b)); asid_table s (asid_high_bits_of x2b) = Some x2c; kheap s x2c = Some (ArchObj x5); (VSRef (x2b && mask local.asid_low_bits) (Some AASIDPool), x51) \<in> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | 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 (pd x)) | _ \<Rightarrow> {}); x51 \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> get_tcb tcb s = Some (?tcb308 x2a x51 x2b x2c x5 x51a x52a x2e)
 2. \<And>x2a x51 x2b x2c x5 x51a x52a x2e. \<lbrakk>invs s; kheap s tcb = Some (TCB x2a); tcb_vtable x2a = ArchObjectCap (PageDirectoryCap x51 (Some x2b)); asid_table s (asid_high_bits_of x2b) = Some x2c; kheap s x2c = Some (ArchObj x5); (VSRef (x2b && mask local.asid_low_bits) (Some AASIDPool), x51) \<in> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | 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 (pd x)) | _ \<Rightarrow> {}); x51 \<noteq> arm_global_pd (arch_state s); s \<turnstile> tcb_vtable (?tcb308 x2a x51 x2b x2c x5 x51a x52a x2e)\<rbrakk> \<Longrightarrow> (asid_table s (asid_high_bits_of x2e) = None \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x2. (kheap s x2 = None \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x2a. (\<forall>x11 x12. x2a = CNode x11 x12 \<longrightarrow> kheap s x2 = Some (CNode x11 x12) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x2c. x2a = TCB x2c \<longrightarrow> kheap s x2 = Some (TCB x2c) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x3. x2a = Endpoint x3 \<longrightarrow> kheap s x2 = Some (Endpoint x3) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x4. x2a = Notification x4 \<longrightarrow> kheap s x2 = Some (Notification x4) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x5. ((VSRef (x2e && mask local.asid_low_bits) (Some AASIDPool), x51a) \<in> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | 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 (pd x)) | _ \<Rightarrow> {}) \<longrightarrow> x2a = ArchObj x5 \<longrightarrow> kheap s x2 = Some (ArchObj x5) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) x51a s) \<and> ((VSRef (x2e && mask local.asid_low_bits) (Some AASIDPool), x51a) \<notin> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | 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 (pd x)) | _ \<Rightarrow> {}) \<longrightarrow> x2a = ArchObj x5 \<longrightarrow> kheap s x2 = Some (ArchObj x5) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s)))) proof (prove)
goal (1 subgoal):
 1. \<And>x2a x51 x2b x2c x5 x51a x52a x2e. \<lbrakk>invs s; kheap s tcb = Some (TCB x2a); tcb_vtable x2a = ArchObjectCap (PageDirectoryCap x51 (Some x2b)); asid_table s (asid_high_bits_of x2b) = Some x2c; kheap s x2c = Some (ArchObj x5); (VSRef (x2b && mask local.asid_low_bits) (Some AASIDPool), x51) \<in> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | 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 (pd x)) | _ \<Rightarrow> {}); x51 \<noteq> arm_global_pd (arch_state s); s \<turnstile> tcb_vtable x2a\<rbrakk> \<Longrightarrow> (asid_table s (asid_high_bits_of x2e) = None \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x2. (kheap s x2 = None \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x2a. (\<forall>x11 x12. x2a = CNode x11 x12 \<longrightarrow> kheap s x2 = Some (CNode x11 x12) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x2c. x2a = TCB x2c \<longrightarrow> kheap s x2 = Some (TCB x2c) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x3. x2a = Endpoint x3 \<longrightarrow> kheap s x2 = Some (Endpoint x3) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x4. x2a = Notification x4 \<longrightarrow> kheap s x2 = Some (Notification x4) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s) \<and> (\<forall>x5. ((VSRef (x2e && mask local.asid_low_bits) (Some AASIDPool), x51a) \<in> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | 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 (pd x)) | _ \<Rightarrow> {}) \<longrightarrow> x2a = ArchObj x5 \<longrightarrow> kheap s x2 = Some (ArchObj x5) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) x51a s) \<and> ((VSRef (x2e && mask local.asid_low_bits) (Some AASIDPool), x51a) \<notin> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | 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 (pd x)) | _ \<Rightarrow> {}) \<longrightarrow> x2a = ArchObj x5 \<longrightarrow> kheap s x2 = Some (ArchObj x5) \<longrightarrow> asid_table s (asid_high_bits_of x2e) = Some x2 \<longrightarrow> x52a = Some x2e \<longrightarrow> x51 = x51a \<and> x2b = x2e \<longrightarrow> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s)))) proof (prove)
goal:
No subgoals!