theory Dpolicy

lemma state_vrefs_asid_pool_transform_rev:
  "\<lbrakk> einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap;
     \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap;
     opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap \<rbrakk> \<Longrightarrow>
     (pdptr, asid && mask ARM_A.asid_low_bits, AASIDPool, Control)
          \<in> state_vrefs s (cap_object poolcap)" apply (subgoal_tac "cap_object poolcap \<noteq> idle_thread s") prefer 2 apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def
                        opt_cap_def slots_of_def) apply (clarsimp simp: map_add_def object_slots_def) apply (case_tac "kheap s (cap_object poolcap)") apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def
                        opt_cap_def slots_of_def) apply (clarsimp simp: map_add_def object_slots_def) apply (clarsimp simp:transform_asid_high_bits_of') apply (simp add:asid_table_transform transform_asid_table_entry_def is_null_cap_def
              split:option.splits) apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def
                       opt_cap_def slots_of_def) apply (drule invs_valid_asid_table) apply (clarsimp simp:valid_asid_table_def) apply (drule bspec) apply fastforce apply (case_tac a, simp_all add:transform_object_def object_slots_def) apply (clarsimp simp:obj_at_def a_type_def split:if_split_asm)+ apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj; simp add:vs_refs_no_global_pts_def graph_of_def) apply (simp add:transform_asid_pool_contents_def unat_map_def transform_asid_low_bits_of
              split:if_split_asm) apply (rule_tac x="(ucast asid, cap_object pdcap)" in image_eqI) apply (simp add:mask_asid_low_bits_ucast_ucast) apply (clarsimp simp:transform_asid_pool_entry_def split:option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap\<rbrakk> \<Longrightarrow> (pdptr, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap; cap_object poolcap \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (pdptr, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap)
 2. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap\<rbrakk> \<Longrightarrow> cap_object poolcap \<noteq> idle_thread s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap\<rbrakk> \<Longrightarrow> cap_object poolcap \<noteq> idle_thread s
 2. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap; cap_object poolcap \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (pdptr, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>transform_asid_table s (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; (case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) (idle_thread s) of None \<Rightarrow> \<lambda>x. None | Some x2 \<Rightarrow> object_slots x2) (snd (transform_asid asid)) = Some pdcap; invs s; valid_list s; valid_sched s; cap_object poolcap = idle_thread s\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap; cap_object poolcap \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (pdptr, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap; cap_object poolcap \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (pdptr, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap; cap_object poolcap \<noteq> idle_thread s; kheap s (cap_object poolcap) = None\<rbrakk> \<Longrightarrow> (pdptr, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap)
 2. \<And>a. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap; cap_object poolcap \<noteq> idle_thread s; kheap s (cap_object poolcap) = Some a\<rbrakk> \<Longrightarrow> (pdptr, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>transform_asid_table s (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; (case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) (cap_object poolcap) of None \<Rightarrow> \<lambda>x. None | Some x2 \<Rightarrow> object_slots x2) (snd (transform_asid asid)) = Some pdcap; cap_object poolcap \<noteq> idle_thread s; kheap s (cap_object poolcap) = None; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap; cap_object poolcap \<noteq> idle_thread s; kheap s (cap_object poolcap) = Some a\<rbrakk> \<Longrightarrow> (pdptr, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap; cap_object poolcap \<noteq> idle_thread s; kheap s (cap_object poolcap) = Some a\<rbrakk> \<Longrightarrow> (pdptr, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>cdl_asid_table (transform s) (unat (asid_high_bits_of asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap; cap_object poolcap \<noteq> idle_thread s; kheap s (cap_object poolcap) = Some a; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap) proof (prove)
goal (1 subgoal):
 1. \<And>a x2. \<lbrakk>\<not> (case poolcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); \<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap; cap_object poolcap \<noteq> idle_thread s; kheap s (cap_object poolcap) = Some a; invs s; valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; AsidPoolCap x2 0 = poolcap\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap) proof (prove)
goal (1 subgoal):
 1. \<And>a x2. \<lbrakk>\<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; object_slots (transform_object (machine_state s) x2 (ekheap s x2) a) (snd (transform_asid asid)) = Some pdcap; x2 \<noteq> idle_thread s; kheap s x2 = Some a; invs s; valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> vs_refs_no_global_pts a proof (prove)
goal (1 subgoal):
 1. \<And>a x2. \<lbrakk>\<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; object_slots (transform_object (machine_state s) x2 (ekheap s x2) a) (snd (transform_asid asid)) = Some pdcap; x2 \<noteq> idle_thread s; kheap s x2 = Some a; valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; valid_asid_table (asid_table s) s\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> vs_refs_no_global_pts a proof (prove)
goal (1 subgoal):
 1. \<And>a x2. \<lbrakk>\<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; object_slots (transform_object (machine_state s) x2 (ekheap s x2) a) (snd (transform_asid asid)) = Some pdcap; x2 \<noteq> idle_thread s; kheap s x2 = Some a; valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> vs_refs_no_global_pts a proof (prove)
goal (2 subgoals):
 1. \<And>a x2. \<lbrakk>\<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; object_slots (transform_object (machine_state s) x2 (ekheap s x2) a) (snd (transform_asid asid)) = Some pdcap; x2 \<noteq> idle_thread s; kheap s x2 = Some a; valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> ?p43 a x2 \<in> ran (asid_table s)
 2. \<And>a x2. \<lbrakk>\<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; object_slots (transform_object (machine_state s) x2 (ekheap s x2) a) (snd (transform_asid asid)) = Some pdcap; x2 \<noteq> idle_thread s; kheap s x2 = Some a; valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) (?p43 a x2) s\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> vs_refs_no_global_pts a proof (prove)
goal (1 subgoal):
 1. \<And>a x2. \<lbrakk>\<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; object_slots (transform_object (machine_state s) x2 (ekheap s x2) a) (snd (transform_asid asid)) = Some pdcap; x2 \<noteq> idle_thread s; kheap s x2 = Some a; valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) x2 s\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> vs_refs_no_global_pts a proof (prove)
goal (3 subgoals):
 1. \<And>a x2 x11 x12. \<lbrakk>\<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; (case case x11 of 0 \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 x12\<rparr> | Suc nat \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) x12, cdl_cnode_size_bits = Suc nat\<rparr> of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) (snd (transform_asid asid)) = Some pdcap; x2 \<noteq> idle_thread s; kheap s x2 = Some (kernel_object.CNode x11 x12); valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) x2 s; a = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> vs_refs_no_global_pts (kernel_object.CNode x11 x12)
 2. \<And>a x2 x2a. \<lbrakk>\<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; (case case ekheap s x2 of Some x2b \<Rightarrow> transform_tcb (machine_state s) x2 x2a x2b of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) (snd (transform_asid asid)) = Some pdcap; x2 \<noteq> idle_thread s; kheap s x2 = Some (TCB x2a); valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) x2 s; a = TCB x2a\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> vs_refs_no_global_pts (TCB x2a)
 3. \<And>a x2 x5. \<lbrakk>\<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; (case case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr> of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) (snd (transform_asid asid)) = Some pdcap; x2 \<noteq> idle_thread s; kheap s x2 = Some (ArchObj x5); valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) x2 s; a = ArchObj x5\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> vs_refs_no_global_pts (ArchObj x5) proof (prove)
goal (1 subgoal):
 1. \<And>x2 x5. \<lbrakk>\<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; (case case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr> of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) (snd (transform_asid asid)) = Some pdcap; x2 \<noteq> idle_thread s; kheap s x2 = Some (ArchObj x5); valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; inj_on (asid_table s) (dom (asid_table s)); (case x5 of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz) = AASIDPool\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> vs_refs_no_global_pts (ArchObj x5) proof (prove)
goal (1 subgoal):
 1. \<And>x2 arch_kernel_obj. \<lbrakk>\<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; (case case arch_kernel_obj of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr> of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) (snd (transform_asid asid)) = Some pdcap; x2 \<noteq> idle_thread s; kheap s x2 = Some (ArchObj arch_kernel_obj); valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; inj_on (asid_table s) (dom (asid_table s)); (case arch_kernel_obj of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz) = AASIDPool\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> vs_refs_no_global_pts (ArchObj arch_kernel_obj) proof (prove)
goal (1 subgoal):
 1. \<And>x2 arch_kernel_obj x1. \<lbrakk>\<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; transform_asid_pool_contents x1 (snd (transform_asid asid)) = Some pdcap; x2 \<noteq> idle_thread s; kheap s x2 = Some (ArchObj (ASIDPool x1)); valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; inj_on (asid_table s) (dom (asid_table s)); arch_kernel_obj = ASIDPool x1\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` {(x, y). x1 x = Some y} proof (prove)
goal (1 subgoal):
 1. \<And>x2 arch_kernel_obj x1. \<lbrakk>x2 \<noteq> idle_thread s; kheap s x2 = Some (ArchObj (ASIDPool x1)); valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; inj_on (asid_table s) (dom (asid_table s)); arch_kernel_obj = ASIDPool x1; \<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; snd (transform_asid asid) < 1024; transform_asid_pool_entry (x1 (UCAST(32 \<rightarrow> 10) asid)) = pdcap\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` {(x, y). x1 x = Some y} proof (prove)
goal (2 subgoals):
 1. \<And>x2 arch_kernel_obj x1. \<lbrakk>x2 \<noteq> idle_thread s; kheap s x2 = Some (ArchObj (ASIDPool x1)); valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; inj_on (asid_table s) (dom (asid_table s)); arch_kernel_obj = ASIDPool x1; \<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; snd (transform_asid asid) < 1024; transform_asid_pool_entry (x1 (UCAST(32 \<rightarrow> 10) asid)) = pdcap\<rbrakk> \<Longrightarrow> (cap_object pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) = (case (UCAST(32 \<rightarrow> 10) asid, cap_object pdcap) of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control))
 2. \<And>x2 arch_kernel_obj x1. \<lbrakk>x2 \<noteq> idle_thread s; kheap s x2 = Some (ArchObj (ASIDPool x1)); valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; inj_on (asid_table s) (dom (asid_table s)); arch_kernel_obj = ASIDPool x1; \<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; snd (transform_asid asid) < 1024; transform_asid_pool_entry (x1 (UCAST(32 \<rightarrow> 10) asid)) = pdcap\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 10) asid, cap_object pdcap) \<in> {(x, y). x1 x = Some y} proof (prove)
goal (1 subgoal):
 1. \<And>x2 arch_kernel_obj x1. \<lbrakk>x2 \<noteq> idle_thread s; kheap s x2 = Some (ArchObj (ASIDPool x1)); valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0; inj_on (asid_table s) (dom (asid_table s)); arch_kernel_obj = ASIDPool x1; \<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); pdptr = cap_object pdcap; snd (transform_asid asid) < 1024; transform_asid_pool_entry (x1 (UCAST(32 \<rightarrow> 10) asid)) = pdcap\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 10) asid, cap_object pdcap) \<in> {(x, y). x1 x = Some y} proof (prove)
goal:
No subgoals!