theory ArchADT_AC

lemma pt_in_pd_same_agent:
  "\<lbrakk> pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings;
     get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ptr vptr = Some (PageTablePDE p x xa) \<rbrakk>
     \<Longrightarrow> pasObjectAbs aag pd_ptr = pasObjectAbs aag (ptrFromPAddr p)" apply (rule_tac aag="pasPolicy aag" in aag_wellformed_Control[rotated]) apply (fastforce simp: pas_refined_def) apply (rule pas_refined_mem[rotated], simp) apply (clarsimp simp: get_pd_entry_def get_arch_obj_def
                 split: option.splits kernel_object.splits arch_kernel_obj.splits) apply (simp add: state_objs_to_policy_def) apply (rule sbta_vref) apply (simp add: state_vrefs_def split: option.splits) apply (clarsimp simp: vs_refs_no_global_pts_def) apply (rule_tac x="(ucast (vptr >> 20), ptrFromPAddr p, 0, {Control})" in bexI) apply simp apply (simp add: kernel_mappings_kernel_mapping_slots' graph_of_def pde_ref2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings; get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ptr vptr = Some (PageTablePDE p x xa)\<rbrakk> \<Longrightarrow> pasObjectAbs aag pd_ptr = pasObjectAbs aag (ptrFromPAddr p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings; get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ptr vptr = Some (PageTablePDE p x xa)\<rbrakk> \<Longrightarrow> policy_wellformed (pasPolicy aag) ?mirqs ?irqs (pasObjectAbs aag pd_ptr)
 2. \<lbrakk>pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings; get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ptr vptr = Some (PageTablePDE p x xa)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag pd_ptr, Control, pasObjectAbs aag (ptrFromPAddr p)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings; get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ptr vptr = Some (PageTablePDE p x xa)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag pd_ptr, Control, pasObjectAbs aag (ptrFromPAddr p)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings; get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ptr vptr = Some (PageTablePDE p x xa)\<rbrakk> \<Longrightarrow> (pd_ptr, Control, ptrFromPAddr p) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings; kheap s pd_ptr = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa\<rbrakk> \<Longrightarrow> (pd_ptr, Control, ptrFromPAddr p) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings; kheap s pd_ptr = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa\<rbrakk> \<Longrightarrow> (pd_ptr, Control, ptrFromPAddr p) \<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. \<And>x3. \<lbrakk>pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings; kheap s pd_ptr = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa\<rbrakk> \<Longrightarrow> (ptrFromPAddr p, ?uu94 x3, ?uv94 x3, Control) \<in> state_vrefs s pd_ptr proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings; kheap s pd_ptr = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa\<rbrakk> \<Longrightarrow> (ptrFromPAddr p, ?uu94 x3, ?uv94 x3, Control) \<in> vs_refs_no_global_pts (ArchObj (PageDirectory x3)) proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings; kheap s pd_ptr = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa\<rbrakk> \<Longrightarrow> \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptrFromPAddr p, ?uu94 x3, ?uv94 x3, Control) \<in> (case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings; kheap s pd_ptr = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa\<rbrakk> \<Longrightarrow> (ptrFromPAddr p, ?uu94 x3, ?uv94 x3, Control) \<in> (case (UCAST(32 \<rightarrow> 12) (vptr >> 20), ptrFromPAddr p, 0, {Control}) of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth))
 2. \<And>x3. \<lbrakk>pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings; kheap s pd_ptr = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (vptr >> 20), ptrFromPAddr p, 0, {Control}) \<in> graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x} proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings; kheap s pd_ptr = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE p x xa\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (vptr >> 20), ptrFromPAddr p, 0, {Control}) \<in> graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x} proof (prove)
goal:
No subgoals!