theory Dpolicy

lemma state_asids_transform:
  "\<lbrakk> einvs s; (x, a, y) \<in> state_asids_to_policy aag s \<rbrakk> \<Longrightarrow>
                               (x, a, y) \<in> cdl_state_asids_to_policy aag (transform s)" apply (unfold state_asids_to_policy_arch_def) apply (drule state_asids_to_policy_aux.induct) prefer 4 apply simp apply (simp add: fst_transform_cslot_ptr) apply (rule_tac cap="transform_cap (ArchObjectCap acap)" in csata_asid) apply (rule caps_of_state_transform_opt_cap) apply simp apply fastforce apply (clarsimp simp: idle_thread_no_asid) apply (fastforce dest: cap_asid'_transform) apply (frule state_vrefs_asidpool_control, simp) apply (simp add: state_vrefs_def, case_tac "kheap s poolptr", simp_all) apply (case_tac aa, simp_all add:vs_refs_no_global_pts_def) apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj, simp_all add:graph_of_def, safe) apply (rule_tac pdcap="cdl_cap.PageDirectoryCap b Fake None" in csata_asid_lookup) apply (simp add: asid_table_entry_transform) apply (simp add: is_null_cap_def transform_asid_table_entry_def) apply (simp add: is_null_cap_def transform_asid_table_entry_def) apply (simp add: ucast_up_ucast_id is_up_def source_size_def target_size_def word_size) apply (simp add: transform_asid_table_entry_def) apply (drule_tac asid="asid" in opt_cap_asid_pool_Some[rotated]) apply (simp add: invs_valid_idle) apply (subst (asm) mask_asid_low_bits_ucast_ucast) apply (subst (asm) up_ucast_inj_eq) apply simp apply (simp add: transform_asid_pool_entry_def) apply (cut_tac aag=aag and asid=asid and asid_tab="cdl_asid_table (transform s)" in csata_asidpool) apply (clarsimp simp: transform_def transform_asid_table_def unat_map_def) apply safe[1] apply (simp add: transform_asid_table_entry_def transform_asid_high_bits_of) apply (simp add: transform_asid_def unat_lt2p[where 'a=7, simplified]) apply (simp add: is_null_cap_def) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; (x, a, y) \<in> state_asids_to_policy aag s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; (x, a, y) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (4 subgoals):
 1. \<And>ptr acap asid. \<lbrakk>einvs s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> ?P (pasObjectAbs aag (fst ptr)) Control (pasASIDAbs aag asid)
 2. \<And>asid poolptr pdptr a. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, a) \<in> state_vrefs s poolptr\<rbrakk> \<Longrightarrow> ?P (pasASIDAbs aag asid) a (pasObjectAbs aag pdptr)
 3. \<And>asid poolptr. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P (pasObjectAbs aag poolptr) (AAuth ASIDPoolMapsASID) (pasASIDAbs aag asid)
 4. \<lbrakk>einvs s; ?P x a y\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>einvs s; ?P x a y\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_asids_to_policy aag (transform s)
 2. \<And>ptr acap asid. \<lbrakk>einvs s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> ?P (pasObjectAbs aag (fst ptr)) Control (pasASIDAbs aag asid)
 3. \<And>asid poolptr pdptr a. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, a) \<in> state_vrefs s poolptr\<rbrakk> \<Longrightarrow> ?P (pasASIDAbs aag asid) a (pasObjectAbs aag pdptr)
 4. \<And>asid poolptr. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P (pasObjectAbs aag poolptr) (AAuth ASIDPoolMapsASID) (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>ptr acap asid. \<lbrakk>einvs s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s)
 2. \<And>asid poolptr pdptr a. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, a) \<in> state_vrefs s poolptr\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, a, pasObjectAbs aag pdptr) \<in> cdl_state_asids_to_policy aag (transform s)
 3. \<And>asid poolptr. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>ptr acap asid. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst (transform_cslot_ptr ptr)), Control, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s)
 2. \<And>asid poolptr pdptr a. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, a) \<in> state_vrefs s poolptr\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, a, pasObjectAbs aag pdptr) \<in> cdl_state_asids_to_policy aag (transform s)
 3. \<And>asid poolptr. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (4 subgoals):
 1. \<And>ptr acap asid. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr ptr) (transform s) = Some (transform_cap (ArchObjectCap acap))
 2. \<And>ptr acap asid. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> asid \<in> cdl_cap_asid' (transform_cap (ArchObjectCap acap))
 3. \<And>asid poolptr pdptr a. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, a) \<in> state_vrefs s poolptr\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, a, pasObjectAbs aag pdptr) \<in> cdl_state_asids_to_policy aag (transform s)
 4. \<And>asid poolptr. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (6 subgoals):
 1. \<And>ptr acap asid. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> caps_of_state s ptr = Some (ArchObjectCap acap)
 2. \<And>ptr acap asid. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> valid_etcbs s
 3. \<And>ptr acap asid. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s
 4. \<And>ptr acap asid. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> asid \<in> cdl_cap_asid' (transform_cap (ArchObjectCap acap))
 5. \<And>asid poolptr pdptr a. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, a) \<in> state_vrefs s poolptr\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, a, pasObjectAbs aag pdptr) \<in> cdl_state_asids_to_policy aag (transform s)
 6. \<And>asid poolptr. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (5 subgoals):
 1. \<And>ptr acap asid. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> valid_etcbs s
 2. \<And>ptr acap asid. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s
 3. \<And>ptr acap asid. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> asid \<in> cdl_cap_asid' (transform_cap (ArchObjectCap acap))
 4. \<And>asid poolptr pdptr a. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, a) \<in> state_vrefs s poolptr\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, a, pasObjectAbs aag pdptr) \<in> cdl_state_asids_to_policy aag (transform s)
 5. \<And>asid poolptr. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (4 subgoals):
 1. \<And>ptr acap asid. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s
 2. \<And>ptr acap asid. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> asid \<in> cdl_cap_asid' (transform_cap (ArchObjectCap acap))
 3. \<And>asid poolptr pdptr a. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, a) \<in> state_vrefs s poolptr\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, a, pasObjectAbs aag pdptr) \<in> cdl_state_asids_to_policy aag (transform s)
 4. \<And>asid poolptr. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>ptr acap asid. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> asid \<in> cdl_cap_asid' (transform_cap (ArchObjectCap acap))
 2. \<And>asid poolptr pdptr a. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, a) \<in> state_vrefs s poolptr\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, a, pasObjectAbs aag pdptr) \<in> cdl_state_asids_to_policy aag (transform s)
 3. \<And>asid poolptr. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>asid poolptr pdptr a. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, a) \<in> state_vrefs s poolptr\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, a, pasObjectAbs aag pdptr) \<in> cdl_state_asids_to_policy aag (transform s)
 2. \<And>asid poolptr. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>asid poolptr pdptr a. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s poolptr; a = Control\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> cdl_state_asids_to_policy aag (transform s)
 2. \<And>asid poolptr. \<lbrakk>einvs s; asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>asid poolptr pdptr a aa. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> vs_refs_no_global_pts aa; a = Control; kheap s poolptr = Some aa\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> cdl_state_asids_to_policy aag (transform s)
 2. \<And>asid poolptr. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>asid poolptr pdptr a aa x5. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, Control) \<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> {}); a = Control; kheap s poolptr = Some (ArchObj x5); aa = ArchObj x5\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> cdl_state_asids_to_policy aag (transform s)
 2. \<And>asid poolptr. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>asid poolptr pdptr a aa arch_kernel_obj. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, Control) \<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> {}); a = Control; kheap s poolptr = Some (ArchObj arch_kernel_obj); aa = ArchObj arch_kernel_obj\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> cdl_state_asids_to_policy aag (transform s)
 2. \<And>asid poolptr. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag b) \<in> cdl_state_asids_to_policy aag (transform s)
 2. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (6 subgoals):
 1. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> cdl_asid_table (transform s) (fst (transform_asid asid)) = Some (?poolcap98 asid poolptr pdptr a aa arch_kernel_obj x1 ab b)
 2. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> \<not> is_null_cap (?poolcap98 asid poolptr pdptr a aa arch_kernel_obj x1 ab b)
 3. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> \<not> is_null_cap (cdl_cap.PageDirectoryCap b Fake None)
 4. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> b = cap_object (cdl_cap.PageDirectoryCap b Fake None)
 5. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> opt_cap (cap_object (?poolcap98 asid poolptr pdptr a aa arch_kernel_obj x1 ab b), snd (transform_asid asid)) (transform s) = Some (cdl_cap.PageDirectoryCap b Fake None)
 6. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (5 subgoals):
 1. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> \<not> is_null_cap (transform_asid_table_entry (Some poolptr))
 2. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> \<not> is_null_cap (cdl_cap.PageDirectoryCap b Fake None)
 3. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> b = cap_object (cdl_cap.PageDirectoryCap b Fake None)
 4. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> opt_cap (cap_object (transform_asid_table_entry (Some poolptr)), snd (transform_asid asid)) (transform s) = Some (cdl_cap.PageDirectoryCap b Fake None)
 5. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (4 subgoals):
 1. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> \<not> is_null_cap (cdl_cap.PageDirectoryCap b Fake None)
 2. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> b = cap_object (cdl_cap.PageDirectoryCap b Fake None)
 3. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> opt_cap (cap_object (transform_asid_table_entry (Some poolptr)), snd (transform_asid asid)) (transform s) = Some (cdl_cap.PageDirectoryCap b Fake None)
 4. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> b = cap_object (cdl_cap.PageDirectoryCap b Fake None)
 2. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> opt_cap (cap_object (transform_asid_table_entry (Some poolptr)), snd (transform_asid asid)) (transform s) = Some (cdl_cap.PageDirectoryCap b Fake None)
 3. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>asid poolptr pdptr a aa arch_kernel_obj x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> opt_cap (cap_object (transform_asid_table_entry (Some poolptr)), snd (transform_asid asid)) (transform s) = Some (cdl_cap.PageDirectoryCap b Fake None)
 2. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>asid poolptr x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; kheap s poolptr = Some (ArchObj (ASIDPool x1)); x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> opt_cap (poolptr, snd (transform_asid asid)) (transform s) = Some (cdl_cap.PageDirectoryCap b Fake None)
 2. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>asid poolptr x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> valid_idle s
 2. \<And>asid poolptr x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab; opt_cap (poolptr, snd (transform_asid asid)) (transform s) = Some (transform_asid_pool_entry (x1 (UCAST(32 \<rightarrow> 10) asid)))\<rbrakk> \<Longrightarrow> opt_cap (poolptr, snd (transform_asid asid)) (transform s) = Some (cdl_cap.PageDirectoryCap b Fake None)
 3. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>asid poolptr x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; x1 ab = Some b; invs s; valid_list s; valid_sched s; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) ab; opt_cap (poolptr, snd (transform_asid asid)) (transform s) = Some (transform_asid_pool_entry (x1 (UCAST(32 \<rightarrow> 10) asid)))\<rbrakk> \<Longrightarrow> opt_cap (poolptr, snd (transform_asid asid)) (transform s) = Some (cdl_cap.PageDirectoryCap b Fake None)
 2. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>asid poolptr x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; x1 ab = Some b; invs s; valid_list s; valid_sched s; UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid) = UCAST(10 \<rightarrow> 32) ab; opt_cap (poolptr, snd (transform_asid asid)) (transform s) = Some (transform_asid_pool_entry (x1 (UCAST(32 \<rightarrow> 10) asid)))\<rbrakk> \<Longrightarrow> opt_cap (poolptr, snd (transform_asid asid)) (transform s) = Some (cdl_cap.PageDirectoryCap b Fake None)
 2. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>asid poolptr x1 ab b. \<lbrakk>opt_cap (poolptr, snd (transform_asid asid)) (transform s) = Some (transform_asid_pool_entry (x1 (UCAST(32 \<rightarrow> 10) asid))); asid_table s (asid_high_bits_of asid) = Some poolptr; x1 ab = Some b; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> LENGTH(10) \<le> LENGTH(32)
 2. \<And>asid poolptr x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; x1 ab = Some b; invs s; valid_list s; valid_sched s; UCAST(32 \<rightarrow> 10) asid = ab; opt_cap (poolptr, snd (transform_asid asid)) (transform s) = Some (transform_asid_pool_entry (x1 (UCAST(32 \<rightarrow> 10) asid)))\<rbrakk> \<Longrightarrow> opt_cap (poolptr, snd (transform_asid asid)) (transform s) = Some (cdl_cap.PageDirectoryCap b Fake None)
 3. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>asid poolptr x1 ab b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; x1 ab = Some b; invs s; valid_list s; valid_sched s; UCAST(32 \<rightarrow> 10) asid = ab; opt_cap (poolptr, snd (transform_asid asid)) (transform s) = Some (transform_asid_pool_entry (x1 (UCAST(32 \<rightarrow> 10) asid)))\<rbrakk> \<Longrightarrow> opt_cap (poolptr, snd (transform_asid asid)) (transform s) = Some (cdl_cap.PageDirectoryCap b Fake None)
 2. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (4 subgoals):
 1. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> cdl_asid_table (transform s) (fst (transform_asid asid)) = Some (?poolcap111 asid poolptr)
 2. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> \<not> is_null_cap (?poolcap111 asid poolptr)
 3. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> asid \<noteq> 0
 4. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s; (pasObjectAbs aag (cap_object (?poolcap111 asid poolptr)), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy_aux aag (?caps111 asid poolptr) (cdl_asid_table (transform s))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (4 subgoals):
 1. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (fst (transform_asid asid) < 128 \<longrightarrow> transform_asid_table_entry (asid_table s (word_of_nat (fst (transform_asid asid)))) = ?poolcap111 asid poolptr) \<and> fst (transform_asid asid) < 128
 2. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> \<not> is_null_cap (?poolcap111 asid poolptr)
 3. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> asid \<noteq> 0
 4. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s; (pasObjectAbs aag (cap_object (?poolcap111 asid poolptr)), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy_aux aag (?caps111 asid poolptr) (cdl_asid_table (transform s))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (5 subgoals):
 1. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s; fst (transform_asid asid) < 128\<rbrakk> \<Longrightarrow> transform_asid_table_entry (asid_table s (word_of_nat (fst (transform_asid asid)))) = ?poolcap111 asid poolptr
 2. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> fst (transform_asid asid) < 128
 3. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> \<not> is_null_cap (?poolcap111 asid poolptr)
 4. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> asid \<noteq> 0
 5. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s; (pasObjectAbs aag (cap_object (?poolcap111 asid poolptr)), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy_aux aag (?caps111 asid poolptr) (cdl_asid_table (transform s))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (4 subgoals):
 1. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> fst (transform_asid asid) < 128
 2. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> \<not> is_null_cap (AsidPoolCap poolptr 0)
 3. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> asid \<noteq> 0
 4. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s; (pasObjectAbs aag (cap_object (AsidPoolCap poolptr 0)), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy_aux aag (?caps111 asid poolptr) (cdl_asid_table (transform s))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> \<not> is_null_cap (AsidPoolCap poolptr 0)
 2. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> asid \<noteq> 0
 3. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s; (pasObjectAbs aag (cap_object (AsidPoolCap poolptr 0)), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy_aux aag (?caps111 asid poolptr) (cdl_asid_table (transform s))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> asid \<noteq> 0
 2. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s; (pasObjectAbs aag (cap_object (AsidPoolCap poolptr 0)), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy_aux aag (?caps111 asid poolptr) (cdl_asid_table (transform s))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0; invs s; valid_list s; valid_sched s; (pasObjectAbs aag (cap_object (AsidPoolCap poolptr 0)), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy_aux aag (?caps111 asid poolptr) (cdl_asid_table (transform s))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> cdl_state_asids_to_policy aag (transform s) proof (prove)
goal:
No subgoals!