theory Dpolicy

lemma state_asids_transform_rev:
  "\<lbrakk> einvs s; (x, a, y) \<in> cdl_state_asids_to_policy aag (transform s) \<rbrakk> \<Longrightarrow>
                               (x, a, y) \<in> state_asids_to_policy aag s" apply (erule cdl_state_asids_to_policy_aux.induct) apply (rule_tac P="is_thread_state_cap cap" in case_split) apply (clarsimp simp:is_thread_state_cap_def split:cdl_cap.splits) apply (rule_tac P="is_bound_ntfn_cap cap" in case_split) apply (clarsimp simp: is_bound_ntfn_cap_def split: cdl_cap.splits) apply (rule_tac P="\<not> is_real_cap cap" in case_split) apply (clarsimp simp:opt_cap_Some_asid_real) apply (rule_tac P="is_null_cap cap" in case_split) apply (clarsimp simp:is_null_cap_def split:cdl_cap.splits) apply (frule caps_of_state_transform_opt_cap_rev, simp+) apply clarsimp apply (subst fst_transform_cslot_ptr[symmetric]) apply (drule (1) cap_asid'_transform[symmetric]) apply (simp only: cap_asid'_member) apply (erule exE) apply (rule sata_asid; fastforce) apply simp apply (rule_tac poolptr="cap_object poolcap" in sata_asid_lookup) 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 (drule_tac t=poolcap in sym) apply simp apply (rule state_vrefs_asid_pool_transform_rev, simp_all) apply (rule sata_asidpool) 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 simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_asids_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>ptr cap asid. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; asid \<in> cdl_cap_asid' cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s
 2. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap asid. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s
 2. \<And>ptr cap asid. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; \<not> is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 4. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>ptr cap asid. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; \<not> is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s
 2. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap asid. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; \<not> is_thread_state_cap cap; is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s
 2. \<And>ptr cap asid. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 4. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>ptr cap asid. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s
 2. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap asid. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap; \<not> is_real_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s
 2. \<And>ptr cap asid. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap; \<not> \<not> is_real_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 4. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>ptr cap asid. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap; \<not> \<not> is_real_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s
 2. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap asid. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap; \<not> \<not> is_real_cap cap; is_null_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s
 2. \<And>ptr cap asid. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap; \<not> \<not> is_real_cap cap; \<not> is_null_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 4. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>ptr cap asid. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap; \<not> \<not> is_real_cap cap; \<not> is_null_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s
 2. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>ptr cap asid. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; opt_cap ptr (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap')\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>a b asid cap' aa ba. \<lbrakk>opt_cap (transform_cslot_ptr (aa, ba)) (transform s) = Some (transform_cap cap'); asid \<in> cdl_cap_asid' (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s (aa, ba) = Some cap'\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst (transform_cslot_ptr (aa, ba))), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>a b asid cap' aa ba. \<lbrakk>opt_cap (transform_cslot_ptr (aa, ba)) (transform s) = Some (transform_cap cap'); asid \<in> cdl_cap_asid' (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s (aa, ba) = Some cap'\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst (aa, ba)), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>a b asid cap' aa ba. \<lbrakk>opt_cap (transform_cslot_ptr (aa, ba)) (transform s) = Some (transform_cap cap'); asid \<in> cdl_cap_asid' (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); valid_list s; valid_sched s; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s (aa, ba) = Some cap'; cdl_cap_asid' (transform_cap cap') = cap_asid' cap'\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst (aa, ba)), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>a b asid cap' aa ba. \<lbrakk>opt_cap (transform_cslot_ptr (aa, ba)) (transform s) = Some (transform_cap cap'); \<exists>acap. cap' = ArchObjectCap acap \<and> asid \<in> acap_asid' acap; \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); valid_list s; valid_sched s; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s (aa, ba) = Some cap'; cdl_cap_asid' (transform_cap cap') = cap_asid' cap'\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst (aa, ba)), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>a b asid cap' aa ba acap. \<lbrakk>opt_cap (transform_cslot_ptr (aa, ba)) (transform s) = Some (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); valid_list s; valid_sched s; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s (aa, ba) = Some cap'; cdl_cap_asid' (transform_cap cap') = cap_asid' cap'; cap' = ArchObjectCap acap \<and> asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst (aa, ba)), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (2 subgoals):
 1. \<And>asid poolcap pdcap pdptr. \<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> (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> state_asids_to_policy aag s
 2. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (2 subgoals):
 1. \<And>asid poolcap pdcap pdptr. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched 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> (pasASIDAbs aag asid, Control, pasObjectAbs aag (cap_object pdcap)) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>asid poolcap pdcap pdptr. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched 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> asid_table s (asid_high_bits_of asid) = Some (cap_object poolcap)
 2. \<And>asid poolcap pdcap pdptr. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched 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 pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap)
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>asid poolcap pdcap. \<lbrakk>cdl_asid_table (transform s) (unat (asid_high_bits_of asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of asid) = Some (cap_object poolcap)
 2. \<And>asid poolcap pdcap pdptr. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched 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 pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap)
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>asid poolcap pdcap x2. \<lbrakk>\<not> (case poolcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); \<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap; invs s; valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; AsidPoolCap x2 0 = poolcap\<rbrakk> \<Longrightarrow> x2 = cap_object poolcap
 2. \<And>asid poolcap pdcap pdptr. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched 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 pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap)
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (3 subgoals):
 1. \<And>asid poolcap pdcap x2. \<lbrakk>\<not> (case poolcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); \<not> (case pdcap of cdl_cap.NullCap \<Rightarrow> True | _ \<Rightarrow> False); opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap; invs s; valid_list s; valid_sched s; asid_table s (asid_high_bits_of asid) = Some x2; poolcap = AsidPoolCap x2 0\<rbrakk> \<Longrightarrow> x2 = cap_object poolcap
 2. \<And>asid poolcap pdcap pdptr. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched 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 pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap)
 3. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (2 subgoals):
 1. \<And>asid poolcap pdcap pdptr. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched 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 pdcap, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap)
 2. \<And>asid poolcap. \<lbrakk>einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag s proof (prove)
goal (1 subgoal):
 1. \<And>asid poolcap. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (cap_object poolcap), AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) proof (prove)
goal (2 subgoals):
 1. \<And>asid poolcap. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of asid) = Some (cap_object poolcap)
 2. \<And>asid poolcap. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> asid \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>asid poolcap. \<lbrakk>cdl_asid_table (transform s) (unat (asid_high_bits_of asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of asid) = Some (cap_object poolcap)
 2. \<And>asid poolcap. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> asid \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>asid poolcap. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> asid \<noteq> 0 proof (prove)
goal:
No subgoals!