theory CNode_AC

lemma set_cap_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and
    (\<lambda>s. (is_transferable_in ptr s \<and> (\<not> Option.is_none (cdt s ptr)))
          \<longrightarrow> is_transferable_cap cap \<or>
              abs_has_auth_to aag Control (fst $ the $ cdt s ptr) (fst ptr)) and
    K (aag_cap_auth aag (pasObjectAbs aag (fst ptr)) cap)\<rbrace>
   set_cap cap ptr
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: pas_refined_def state_objs_to_policy_def aag_cap_auth_def) apply (rule hoare_pre) apply (wp set_cap_caps_of_state set_cap_state_vrefs  | wps)+ apply clarsimp apply (intro conjI)  \<comment> \<open>auth_graph_map\<close> apply (clarsimp dest!: auth_graph_map_memD) apply (erule state_bits_to_policy.cases;
           solves\<open>auto simp: cap_links_asid_slot_def label_owns_asid_slot_def
                      intro: auth_graph_map_memI state_bits_to_policy.intros
                      split: if_split_asm\<close>) apply (erule (2) sata_update[unfolded fun_upd_def]) apply (erule (2) sita_caps_update[unfolded fun_upd_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_transferable_in ptr s \<and> \<not> Option.is_none (cdt s ptr) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst $ the $ cdt s ptr), Control, pasObjectAbs aag (fst ptr)) \<in> pasPolicy aag) and K (aag_cap_auth aag (pasObjectAbs aag (fst ptr)) cap)\<rbrace> set_cap cap ptr \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag) and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_transferable_in ptr s \<and> \<not> Option.is_none (cdt s ptr) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst (the (cdt s ptr))), Control, pasObjectAbs aag (fst ptr)) \<in> pasPolicy aag) and (\<lambda>y. (\<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst ptr), auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst ptr), Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap \<and> cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap)\<rbrace> set_cap cap ptr \<lbrace>\<lambda>_ s. pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q6\<rbrace> set_cap cap ptr \<lbrace>\<lambda>_ s. pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrace>
 2. \<And>s. ((\<lambda>s. pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag) and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_transferable_in ptr s \<and> \<not> Option.is_none (cdt s ptr) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst (the (cdt s ptr))), Control, pasObjectAbs aag (fst ptr)) \<in> pasPolicy aag) and (\<lambda>y. (\<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst ptr), auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst ptr), Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap \<and> cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag) and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_transferable_in ptr s \<and> \<not> Option.is_none (cdt s ptr) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst (the (cdt s ptr))), Control, pasObjectAbs aag (fst ptr)) \<in> pasPolicy aag) and (\<lambda>y. (\<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst ptr), auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst ptr), Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap \<and> cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap)) s \<Longrightarrow> pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> (pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>sa. auth_graph_map (pasObjectAbs aag) (state_bits_to_policy ((caps_of_state s)(ptr \<mapsto> cap)) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs sa)) \<subseteq> pasPolicy aag \<and> state_asids_to_policy_arch aag ((caps_of_state s)(ptr \<mapsto> cap)) (arch_state s) (state_vrefs sa) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy_aux aag ((caps_of_state s)(ptr \<mapsto> cap)) \<subseteq> pasPolicy aag)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_transferable_in ptr s \<and> \<not> Option.is_none (cdt s ptr) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst (the (cdt s ptr))), Control, pasObjectAbs aag (fst ptr)) \<in> pasPolicy aag; \<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst ptr), auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst ptr), Control, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap; cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (\<lambda>a. if a = ptr then Some cap else caps_of_state s a) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag \<and> state_asids_to_policy_arch aag (\<lambda>a. if a = ptr then Some cap else caps_of_state s a) (arch_state s) (state_vrefs s) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy_aux aag (\<lambda>a. if a = ptr then Some cap else caps_of_state s a) \<subseteq> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_transferable_in ptr s \<and> \<not> Option.is_none (cdt s ptr) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst (the (cdt s ptr))), Control, pasObjectAbs aag (fst ptr)) \<in> pasPolicy aag; \<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst ptr), auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst ptr), Control, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap; cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (\<lambda>a. if a = ptr then Some cap else caps_of_state s a) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag
 2. \<And>s. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_transferable_in ptr s \<and> \<not> Option.is_none (cdt s ptr) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst (the (cdt s ptr))), Control, pasObjectAbs aag (fst ptr)) \<in> pasPolicy aag; \<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst ptr), auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst ptr), Control, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap; cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap\<rbrakk> \<Longrightarrow> state_asids_to_policy_arch aag (\<lambda>a. if a = ptr then Some cap else caps_of_state s a) (arch_state s) (state_vrefs s) \<subseteq> pasPolicy aag
 3. \<And>s. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_transferable_in ptr s \<and> \<not> Option.is_none (cdt s ptr) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst (the (cdt s ptr))), Control, pasObjectAbs aag (fst ptr)) \<in> pasPolicy aag; \<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst ptr), auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst ptr), Control, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap; cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap\<rbrakk> \<Longrightarrow> state_irqs_to_policy_aux aag (\<lambda>a. if a = ptr then Some cap else caps_of_state s a) \<subseteq> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>s aa x' y'. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_transferable_in ptr s \<and> \<not> Option.is_none (cdt s ptr) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst (the (cdt s ptr))), Control, pasObjectAbs aag (fst ptr)) \<in> pasPolicy aag; \<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst ptr), auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst ptr), Control, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap; cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap; (x', aa, y') \<in> state_bits_to_policy (\<lambda>a. if a = ptr then Some cap else caps_of_state s a) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag
 2. \<And>s. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_transferable_in ptr s \<and> \<not> Option.is_none (cdt s ptr) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst (the (cdt s ptr))), Control, pasObjectAbs aag (fst ptr)) \<in> pasPolicy aag; \<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst ptr), auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst ptr), Control, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap; cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap\<rbrakk> \<Longrightarrow> state_asids_to_policy_arch aag (\<lambda>a. if a = ptr then Some cap else caps_of_state s a) (arch_state s) (state_vrefs s) \<subseteq> pasPolicy aag
 3. \<And>s. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_transferable_in ptr s \<and> \<not> Option.is_none (cdt s ptr) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst (the (cdt s ptr))), Control, pasObjectAbs aag (fst ptr)) \<in> pasPolicy aag; \<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst ptr), auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst ptr), Control, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap; cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap\<rbrakk> \<Longrightarrow> state_irqs_to_policy_aux aag (\<lambda>a. if a = ptr then Some cap else caps_of_state s a) \<subseteq> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_transferable_in ptr s \<and> \<not> Option.is_none (cdt s ptr) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst (the (cdt s ptr))), Control, pasObjectAbs aag (fst ptr)) \<in> pasPolicy aag; \<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst ptr), auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst ptr), Control, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap; cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap\<rbrakk> \<Longrightarrow> state_asids_to_policy_arch aag (\<lambda>a. if a = ptr then Some cap else caps_of_state s a) (arch_state s) (state_vrefs s) \<subseteq> pasPolicy aag
 2. \<And>s. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_transferable_in ptr s \<and> \<not> Option.is_none (cdt s ptr) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst (the (cdt s ptr))), Control, pasObjectAbs aag (fst ptr)) \<in> pasPolicy aag; \<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst ptr), auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst ptr), Control, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap; cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap\<rbrakk> \<Longrightarrow> state_irqs_to_policy_aux aag (\<lambda>a. if a = ptr then Some cap else caps_of_state s a) \<subseteq> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_transferable_in ptr s \<and> \<not> Option.is_none (cdt s ptr) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst (the (cdt s ptr))), Control, pasObjectAbs aag (fst ptr)) \<in> pasPolicy aag; \<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst ptr), auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst ptr), Control, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap; cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap\<rbrakk> \<Longrightarrow> state_irqs_to_policy_aux aag (\<lambda>a. if a = ptr then Some cap else caps_of_state s a) \<subseteq> pasPolicy aag proof (prove)
goal:
No subgoals!