theory ArchADT_AC

lemma get_page_info_state_objs_to_policy:
  "\<lbrakk> invs s; auth \<in> vspace_cap_rights_to_auth r;
     get_page_info (\<lambda>obj. get_arch_obj (kheap s obj))
                   (get_pd_of_thread (kheap s) (arch_state s) tcb) x =
     Some (base, sz, attr, r);
     get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s);
     get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj))
                  (get_pd_of_thread (kheap s) (arch_state s) tcb) x =
     Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings \<rbrakk>
     \<Longrightarrow> (ptrFromPAddr word1, auth, ptrFromPAddr (base + (x && mask sz))) \<in> state_objs_to_policy s" apply (simp add: state_objs_to_policy_def) apply (rule sbta_vref) apply (clarsimp simp: state_vrefs_def split: option.splits) apply (frule pt_in_pd_page_table_at) apply (simp add: get_pd_of_thread_reachable)+ apply (clarsimp simp: typ_at_eq_kheap_obj) apply (clarsimp simp: vs_refs_no_global_pts_def) apply (rule_tac x="(ucast ((x >> 12) && mask 8),  ptrFromPAddr base, sz,
                      vspace_cap_rights_to_auth r)" in bexI) apply clarsimp apply (rule_tac x="(ptrFromPAddr base + (x && mask sz), auth)" in image_eqI) apply (simp add: ptrFromPAddr_def) apply (simp add: ptr_offset_in_ptr_range) apply (clarsimp simp: get_page_info_def get_pd_entry_def get_pt_info_def
                        get_pt_entry_def get_arch_obj_def pte_ref_def graph_of_def
                 split: option.splits pte.splits pde.splits arch_kernel_obj.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> (ptrFromPAddr word1, auth, ptrFromPAddr (base + (x && mask sz))) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> (ptrFromPAddr word1, auth, ptrFromPAddr (base + (x && mask sz))) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> (ptrFromPAddr (base + (x && mask sz)), ?uu, ?uv, auth) \<in> state_vrefs s (ptrFromPAddr word1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> (\<exists>y. kheap s (ptrFromPAddr word1) = Some y) \<and> (\<forall>x2. kheap s (ptrFromPAddr word1) = Some x2 \<longrightarrow> (ptrFromPAddr (base + (x && mask sz)), ?uu, ?uv, auth) \<in> vs_refs_no_global_pts x2) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) ?pd_ptr9 ?x9 = Some (PageTablePDE ?word1.9 ?set1.9 ?word2.9)
 2. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> ?pd_ptr9) s
 3. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ?x9 \<notin> kernel_mappings
 4. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; typ_at (AArch APageTable) (ptrFromPAddr ?word1.9) s\<rbrakk> \<Longrightarrow> (\<exists>y. kheap s (ptrFromPAddr word1) = Some y) \<and> (\<forall>x2. kheap s (ptrFromPAddr word1) = Some x2 \<longrightarrow> (ptrFromPAddr (base + (x && mask sz)), ?uu, ?uv, auth) \<in> vs_refs_no_global_pts x2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; typ_at (AArch APageTable) (ptrFromPAddr word1) s\<rbrakk> \<Longrightarrow> (\<exists>y. kheap s (ptrFromPAddr word1) = Some y) \<and> (\<forall>x2. kheap s (ptrFromPAddr word1) = Some x2 \<longrightarrow> (ptrFromPAddr (base + (x && mask sz)), ?uu, ?uv, auth) \<in> vs_refs_no_global_pts x2) proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; kheap s (ptrFromPAddr word1) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (ptrFromPAddr (base + (x && mask sz)), ?uu, ?uv, auth) \<in> vs_refs_no_global_pts (ArchObj (PageTable pt)) proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; kheap s (ptrFromPAddr word1) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> \<exists>xa\<in>graph_of (pte_ref \<circ> pt). (ptrFromPAddr (base + (x && mask sz)), ?uu, ?uv, auth) \<in> (case xa of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) r, APageTable, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (2 subgoals):
 1. \<And>pt. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; kheap s (ptrFromPAddr word1) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (ptrFromPAddr (base + (x && mask sz)), ?uu, ?uv, auth) \<in> (case (UCAST(32 \<rightarrow> 8) ((x >> 12) && mask 8), ptrFromPAddr base, sz, vspace_cap_rights_to_auth r) of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) r, APageTable, a)) ` (ptr_range p sz \<times> auth))
 2. \<And>pt. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; kheap s (ptrFromPAddr word1) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 8) ((x >> 12) && mask 8), ptrFromPAddr base, sz, vspace_cap_rights_to_auth r) \<in> graph_of (pte_ref \<circ> pt) proof (prove)
goal (2 subgoals):
 1. \<And>pt. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; kheap s (ptrFromPAddr word1) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (ptrFromPAddr (base + (x && mask sz)), ?uu, ?uv, auth) \<in> (\<lambda>xa. case xa of (p, a) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) ((x >> 12) && mask 8)), APageTable, a)) ` (ptr_range (ptrFromPAddr base) sz \<times> vspace_cap_rights_to_auth r)
 2. \<And>pt. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; kheap s (ptrFromPAddr word1) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 8) ((x >> 12) && mask 8), ptrFromPAddr base, sz, vspace_cap_rights_to_auth r) \<in> graph_of (pte_ref \<circ> pt) proof (prove)
goal (3 subgoals):
 1. \<And>pt. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; kheap s (ptrFromPAddr word1) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (ptrFromPAddr (base + (x && mask sz)), ?uu, ?uv, auth) = (case (ptrFromPAddr base + (x && mask sz), auth) of (p, a) \<Rightarrow> (p, UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) ((x >> 12) && mask 8)), APageTable, a))
 2. \<And>pt. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; kheap s (ptrFromPAddr word1) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (ptrFromPAddr base + (x && mask sz), auth) \<in> ptr_range (ptrFromPAddr base) sz \<times> vspace_cap_rights_to_auth r
 3. \<And>pt. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; kheap s (ptrFromPAddr word1) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 8) ((x >> 12) && mask 8), ptrFromPAddr base, sz, vspace_cap_rights_to_auth r) \<in> graph_of (pte_ref \<circ> pt) proof (prove)
goal (2 subgoals):
 1. \<And>pt. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; kheap s (ptrFromPAddr word1) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (ptrFromPAddr base + (x && mask sz), auth) \<in> ptr_range (ptrFromPAddr base) sz \<times> vspace_cap_rights_to_auth r
 2. \<And>pt. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; kheap s (ptrFromPAddr word1) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 8) ((x >> 12) && mask 8), ptrFromPAddr base, sz, vspace_cap_rights_to_auth r) \<in> graph_of (pte_ref \<circ> pt) proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>invs s; auth \<in> vspace_cap_rights_to_auth r; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings; kheap s (ptrFromPAddr word1) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 8) ((x >> 12) && mask 8), ptrFromPAddr base, sz, vspace_cap_rights_to_auth r) \<in> graph_of (pte_ref \<circ> pt) proof (prove)
goal:
No subgoals!