theory Dpolicy

lemma state_vrefs_asidpool_control:
  "(pdptr, asid, AASIDPool, auth) \<in> state_vrefs s poolptr \<Longrightarrow> auth = Control" apply (clarsimp simp:state_vrefs_def ) apply (cases "kheap s poolptr") apply clarsimp apply (simp add: vs_refs_no_global_pts_def, case_tac a; clarsimp) apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (pdptr, asid, AASIDPool, auth) \<in> state_vrefs s poolptr \<Longrightarrow> auth = Control proof (prove)
goal (1 subgoal):
 1. (pdptr, asid, AASIDPool, auth) \<in> (case kheap s poolptr of None \<Rightarrow> {} | Some x2 \<Rightarrow> vs_refs_no_global_pts x2) \<Longrightarrow> auth = Control proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(pdptr, asid, AASIDPool, auth) \<in> (case kheap s poolptr of None \<Rightarrow> {} | Some x2 \<Rightarrow> vs_refs_no_global_pts x2); kheap s poolptr = None\<rbrakk> \<Longrightarrow> auth = Control
 2. \<And>a. \<lbrakk>(pdptr, asid, AASIDPool, auth) \<in> (case kheap s poolptr of None \<Rightarrow> {} | Some x2 \<Rightarrow> vs_refs_no_global_pts x2); kheap s poolptr = Some a\<rbrakk> \<Longrightarrow> auth = Control proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>(pdptr, asid, AASIDPool, auth) \<in> (case kheap s poolptr of None \<Rightarrow> {} | Some x2 \<Rightarrow> vs_refs_no_global_pts x2); kheap s poolptr = Some a\<rbrakk> \<Longrightarrow> auth = Control proof (prove)
goal (1 subgoal):
 1. \<And>x5. \<lbrakk>(pdptr, asid, AASIDPool, auth) \<in> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, p). (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool | arch_kernel_obj.PageTable pt \<Rightarrow> \<Union>(r, p, sz, auth)\<in>graph_of (pte_ref \<circ> pt). (\<lambda>(p, a). (p, UCAST(8 \<rightarrow> 32) r, APageTable, a)) ` (ptr_range p sz \<times> auth) | arch_kernel_obj.PageDirectory pd \<Rightarrow> \<Union>(r, p, sz, auth)\<in>graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (\<lambda>(p, a). (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth) | DataPage bool vmpage_size \<Rightarrow> {}); kheap s poolptr = Some (ArchObj x5)\<rbrakk> \<Longrightarrow> auth = Control proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj. \<lbrakk>(pdptr, asid, AASIDPool, auth) \<in> (case arch_kernel_obj of ASIDPool pool \<Rightarrow> (\<lambda>(r, p). (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool | arch_kernel_obj.PageTable pt \<Rightarrow> \<Union>(r, p, sz, auth)\<in>graph_of (pte_ref \<circ> pt). (\<lambda>(p, a). (p, UCAST(8 \<rightarrow> 32) r, APageTable, a)) ` (ptr_range p sz \<times> auth) | arch_kernel_obj.PageDirectory pd \<Rightarrow> \<Union>(r, p, sz, auth)\<in>graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (\<lambda>(p, a). (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth) | DataPage bool vmpage_size \<Rightarrow> {}); kheap s poolptr = Some (ArchObj arch_kernel_obj)\<rbrakk> \<Longrightarrow> auth = Control proof (prove)
goal:
No subgoals!