theory Dpolicy

lemma state_vrefs_transform:
  "\<lbrakk> invs s; ptr \<noteq> idle_thread s; (ptr', ref, aat, auth) \<in> state_vrefs s ptr \<rbrakk> \<Longrightarrow>
     (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s)" apply (simp add:state_vrefs_def, case_tac "kheap s ptr", simp+) apply (case_tac a, simp_all add:vs_refs_no_global_pts_def) apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj; simp add: vs_refs_no_global_pts_def) apply (clarsimp simp:graph_of_def) apply (subst fst') apply (rule csta_caps) apply (drule_tac asid="ucast aa" in opt_cap_asid_pool_Some[rotated]) apply (simp add:invs_valid_idle) apply (simp add:ucast_up_ucast_id is_up_def source_size_def target_size_def word_size) apply (simp add:transform_asid_pool_entry_def) apply (simp add:transform_asid_pool_entry_def cdl_cap_auth_conferred_def) apply (clarsimp simp:graph_of_def) apply (subst fst') apply (rule csta_caps) apply (drule_tac slot=aa in opt_cap_pt_Some'[rotated]) apply (simp add:invs_valid_idle) apply simp apply (rule_tac a=ab and b=ac and c=b in pte_cdl_obj_refs, simp+) apply (rule_tac a=ab and b=ac and c=b in pte_cdl_cap_auth_conferred, simp+) apply (erule bexE) apply (clarsimp simp:graph_of_def) apply (subst fst') apply (rule csta_caps) apply (drule_tac slot=aa in opt_cap_pd_Some'[rotated]) apply (simp add:word_not_le[symmetric]) apply (simp add:invs_valid_idle) apply simp apply (rule_tac a=ab and b=ac and c=b in pde_cdl_obj_refs, simp+) apply (rule_tac a=ab and b=ac and c=b in pde_cdl_cap_auth_conferred, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; ptr \<noteq> idle_thread s; (ptr', ref, aat, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>invs s; ptr \<noteq> idle_thread s; (ptr', ref, aat, auth) \<in> vs_refs_no_global_pts a; kheap s ptr = Some a\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>a x5. \<lbrakk>invs s; ptr \<noteq> idle_thread s; (ptr', ref, aat, 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 ptr = Some (ArchObj x5); a = ArchObj x5\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>a arch_kernel_obj. \<lbrakk>invs s; ptr \<noteq> idle_thread s; (ptr', ref, aat, 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 ptr = Some (ArchObj arch_kernel_obj); a = ArchObj arch_kernel_obj\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>a arch_kernel_obj x1. \<lbrakk>invs s; ptr \<noteq> idle_thread s; (ptr', ref, aat, auth) \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of x1; kheap s ptr = Some (ArchObj (ASIDPool x1)); a = ArchObj (ASIDPool x1); arch_kernel_obj = ASIDPool x1\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>a arch_kernel_obj x2. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pte_ref \<circ> x2). (ptr', ref, aat, auth) \<in> (case x 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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); a = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (ASIDPool x1)); x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control\<rbrakk> \<Longrightarrow> (ptr, Control, ptr') \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>a arch_kernel_obj x2. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pte_ref \<circ> x2). (ptr', ref, aat, auth) \<in> (case x 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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); a = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (ASIDPool x1)); x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control\<rbrakk> \<Longrightarrow> (fst (ptr, ?b37 x1 aa), Control, ptr') \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>a arch_kernel_obj x2. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pte_ref \<circ> x2). (ptr', ref, aat, auth) \<in> (case x 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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); a = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (5 subgoals):
 1. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (ASIDPool x1)); x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control\<rbrakk> \<Longrightarrow> opt_cap (ptr, ?b37 x1 aa) (transform s) = Some (?cap39 x1 aa)
 2. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (ASIDPool x1)); x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control\<rbrakk> \<Longrightarrow> ptr' \<in> cdl_obj_refs (?cap39 x1 aa)
 3. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (ASIDPool x1)); x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control\<rbrakk> \<Longrightarrow> Control \<in> cdl_cap_auth_conferred (?cap39 x1 aa)
 4. \<And>a arch_kernel_obj x2. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pte_ref \<circ> x2). (ptr', ref, aat, auth) \<in> (case x 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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); a = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (6 subgoals):
 1. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control\<rbrakk> \<Longrightarrow> valid_idle s
 2. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control; opt_cap (ptr, snd (transform_asid (UCAST(10 \<rightarrow> 32) aa))) (transform s) = Some (transform_asid_pool_entry (x1 (UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) aa))))\<rbrakk> \<Longrightarrow> opt_cap (ptr, ?b37 x1 aa) (transform s) = Some (?cap39 x1 aa)
 3. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (ASIDPool x1)); x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control\<rbrakk> \<Longrightarrow> ptr' \<in> cdl_obj_refs (?cap39 x1 aa)
 4. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (ASIDPool x1)); x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control\<rbrakk> \<Longrightarrow> Control \<in> cdl_cap_auth_conferred (?cap39 x1 aa)
 5. \<And>a arch_kernel_obj x2. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pte_ref \<circ> x2). (ptr', ref, aat, auth) \<in> (case x 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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); a = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (5 subgoals):
 1. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control; opt_cap (ptr, snd (transform_asid (UCAST(10 \<rightarrow> 32) aa))) (transform s) = Some (transform_asid_pool_entry (x1 (UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) aa))))\<rbrakk> \<Longrightarrow> opt_cap (ptr, ?b37 x1 aa) (transform s) = Some (?cap39 x1 aa)
 2. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (ASIDPool x1)); x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control\<rbrakk> \<Longrightarrow> ptr' \<in> cdl_obj_refs (?cap39 x1 aa)
 3. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (ASIDPool x1)); x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control\<rbrakk> \<Longrightarrow> Control \<in> cdl_cap_auth_conferred (?cap39 x1 aa)
 4. \<And>a arch_kernel_obj x2. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pte_ref \<circ> x2). (ptr', ref, aat, auth) \<in> (case x 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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); a = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (4 subgoals):
 1. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (ASIDPool x1)); x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control\<rbrakk> \<Longrightarrow> ptr' \<in> cdl_obj_refs (transform_asid_pool_entry (Some ptr'))
 2. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (ASIDPool x1)); x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control\<rbrakk> \<Longrightarrow> Control \<in> cdl_cap_auth_conferred (transform_asid_pool_entry (Some ptr'))
 3. \<And>a arch_kernel_obj x2. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pte_ref \<circ> x2). (ptr', ref, aat, auth) \<in> (case x 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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); a = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>x1 aa. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (ASIDPool x1)); x1 aa = Some ptr'; ref = UCAST(10 \<rightarrow> 32) aa; aat = AASIDPool; auth = Control\<rbrakk> \<Longrightarrow> Control \<in> cdl_cap_auth_conferred (transform_asid_pool_entry (Some ptr'))
 2. \<And>a arch_kernel_obj x2. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pte_ref \<circ> x2). (ptr', ref, aat, auth) \<in> (case x 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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); a = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>a arch_kernel_obj x2. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pte_ref \<circ> x2). (ptr', ref, aat, auth) \<in> (case x 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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); a = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable\<rbrakk> \<Longrightarrow> (fst (ptr, ?b66 x2 aa ab ac b), auth, ptr') \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (4 subgoals):
 1. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable\<rbrakk> \<Longrightarrow> opt_cap (ptr, ?b66 x2 aa ab ac b) (transform s) = Some (?cap68 x2 aa ab ac b)
 2. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable\<rbrakk> \<Longrightarrow> ptr' \<in> cdl_obj_refs (?cap68 x2 aa ab ac b)
 3. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (?cap68 x2 aa ab ac b)
 4. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (5 subgoals):
 1. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable\<rbrakk> \<Longrightarrow> valid_idle s
 2. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable; opt_cap (ptr, unat aa) (transform s) = Some (transform_pte (x2 aa))\<rbrakk> \<Longrightarrow> opt_cap (ptr, ?b66 x2 aa ab ac b) (transform s) = Some (?cap68 x2 aa ab ac b)
 3. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable\<rbrakk> \<Longrightarrow> ptr' \<in> cdl_obj_refs (?cap68 x2 aa ab ac b)
 4. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (?cap68 x2 aa ab ac b)
 5. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (4 subgoals):
 1. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable; opt_cap (ptr, unat aa) (transform s) = Some (transform_pte (x2 aa))\<rbrakk> \<Longrightarrow> opt_cap (ptr, ?b66 x2 aa ab ac b) (transform s) = Some (?cap68 x2 aa ab ac b)
 2. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable\<rbrakk> \<Longrightarrow> ptr' \<in> cdl_obj_refs (?cap68 x2 aa ab ac b)
 3. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (?cap68 x2 aa ab ac b)
 4. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable\<rbrakk> \<Longrightarrow> ptr' \<in> cdl_obj_refs (transform_pte (x2 aa))
 2. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (transform_pte (x2 aa))
 3. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>x2 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable x2)); pte_ref (x2 aa) = Some (ab, ac, b); ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(8 \<rightarrow> 32) aa; aat = APageTable\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (transform_pte (x2 aa))
 2. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>a arch_kernel_obj x3. \<lbrakk>invs s; ptr \<noteq> idle_thread s; \<exists>x\<in>graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. (ptr', ref, aat, auth) \<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)); kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>a arch_kernel_obj x3 x. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3; x \<in> graph_of (pde_ref2 \<circ> x3) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}; (ptr', ref, aat, auth) \<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))\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> (fst (ptr, ?b92 x3 aa ab ac b), auth, ptr') \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> opt_cap (ptr, ?b92 x3 aa ab ac b) (transform s) = Some (?cap93 x3 aa ab ac b)
 2. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> ptr' \<in> cdl_obj_refs (?cap93 x3 aa ab ac b)
 3. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (?cap93 x3 aa ab ac b) proof (prove)
goal (5 subgoals):
 1. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> aa < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)
 2. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> valid_idle s
 3. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory; opt_cap (ptr, unat aa) (transform s) = Some (transform_pde (x3 aa))\<rbrakk> \<Longrightarrow> opt_cap (ptr, ?b92 x3 aa ab ac b) (transform s) = Some (?cap93 x3 aa ab ac b)
 4. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> ptr' \<in> cdl_obj_refs (?cap93 x3 aa ab ac b)
 5. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (?cap93 x3 aa ab ac b) proof (prove)
goal (4 subgoals):
 1. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> valid_idle s
 2. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory; opt_cap (ptr, unat aa) (transform s) = Some (transform_pde (x3 aa))\<rbrakk> \<Longrightarrow> opt_cap (ptr, ?b92 x3 aa ab ac b) (transform s) = Some (?cap93 x3 aa ab ac b)
 3. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> ptr' \<in> cdl_obj_refs (?cap93 x3 aa ab ac b)
 4. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (?cap93 x3 aa ab ac b) proof (prove)
goal (3 subgoals):
 1. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory; opt_cap (ptr, unat aa) (transform s) = Some (transform_pde (x3 aa))\<rbrakk> \<Longrightarrow> opt_cap (ptr, ?b92 x3 aa ab ac b) (transform s) = Some (?cap93 x3 aa ab ac b)
 2. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> ptr' \<in> cdl_obj_refs (?cap93 x3 aa ab ac b)
 3. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (?cap93 x3 aa ab ac b) proof (prove)
goal (2 subgoals):
 1. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> ptr' \<in> cdl_obj_refs (transform_pde (x3 aa))
 2. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (transform_pde (x3 aa)) proof (prove)
goal (1 subgoal):
 1. \<And>x3 aa ab ac b. \<lbrakk>invs s; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); pde_ref2 (x3 aa) = Some (ab, ac, b); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> aa; ptr' \<in> ptr_range ab ac; auth \<in> b; ref = UCAST(12 \<rightarrow> 32) aa; aat = APageDirectory\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (transform_pde (x3 aa)) proof (prove)
goal:
No subgoals!