theory CNode_AC

lemma set_cdt_pas_refined:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrace>pas_refined aag and (\<lambda>s. \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y
           \<longrightarrow> (is_transferable (caps_of_state s x) \<or>
                abs_has_auth_to aag Control (fst y) (fst x)) \<and>
               abs_has_auth_to aag DeleteDerived (fst y) (fst x))\<rbrace>
         set_cdt c
         \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: pas_refined_def state_objs_to_policy_def set_cdt_def) apply (wp | simp | simp_all)+ apply (clarsimp dest!: auth_graph_map_memD) apply (subgoal_tac
          "\<forall>x y. c x = Some y \<longrightarrow>
            (is_transferable (caps_of_state s x) \<or> abs_has_auth_to aag Control (fst y) (fst x))
          \<and> abs_has_auth_to  aag DeleteDerived (fst y) (fst x)") defer apply (intro allI, case_tac "cdt s x = Some y") apply (solves\<open>auto intro: auth_graph_map_memI state_bits_to_policy.intros\<close>) apply (fastforce dest!: spec elim!: mp) apply (erule state_bits_to_policy.cases) apply (auto intro: auth_graph_map_memI state_bits_to_policy.intros
              split: if_split_asm | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and (\<lambda>s. \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag)\<rbrace> set_cdt c \<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 (\<lambda>s. \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag)\<rbrace> do s <- get;
put (s\<lparr>cdt := c\<rparr>)
od \<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 (1 subgoal):
 1. \<And>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> (\<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<Longrightarrow> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) c (state_vrefs s)) \<subseteq> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s aa x' y'. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; (x', aa, y') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) c (state_vrefs 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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s aa x' y'. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; (x', aa, y') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) c (state_vrefs 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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; \<forall>x y. c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag
 2. \<And>s aa x' y'. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; (x', aa, y') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) c (state_vrefs 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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<forall>x y. c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s aa x' y'. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; (x', aa, y') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) c (state_vrefs 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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<forall>x y. c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag
 2. \<And>s aa x' y'. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; (x', aa, y') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) c (state_vrefs 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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; \<forall>x y. c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>s aa x' y' x y. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; (x', aa, y') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) c (state_vrefs 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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; cdt s x = Some y\<rbrakk> \<Longrightarrow> c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag
 2. \<And>s aa x' y' x y. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; (x', aa, y') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) c (state_vrefs 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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; cdt s x \<noteq> Some y\<rbrakk> \<Longrightarrow> c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag
 3. \<And>s aa x' y'. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; (x', aa, y') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) c (state_vrefs 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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; \<forall>x y. c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s aa x' y' x y. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; (x', aa, y') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) c (state_vrefs 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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; cdt s x \<noteq> Some y\<rbrakk> \<Longrightarrow> c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag
 2. \<And>s aa x' y'. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; (x', aa, y') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) c (state_vrefs 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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; \<forall>x y. c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s aa x' y'. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; (x', aa, y') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) c (state_vrefs 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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; \<forall>x y. c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag proof (prove)
goal (7 subgoals):
 1. \<And>s aa x' y' ptr cap oref auth. \<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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; \<forall>x y. c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; x' = fst ptr; aa = auth; y' = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag
 2. \<And>s aa x' y' ptr cap oref. \<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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; \<forall>x y. c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; x' = fst ptr; aa = Control; y' = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag
 3. \<And>s aa x' y' oref' auth oref. \<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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; \<forall>x y. c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; x' = oref; aa = auth; y' = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag
 4. \<And>s aa x' y' oref oref' auth. \<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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; \<forall>x y. c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; x' = oref; aa = auth; y' = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag
 5. \<And>s aa x' y' slot' slot. \<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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; \<forall>x y. c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; x' = fst slot; aa = Control; y' = fst slot'; c slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag
 6. \<And>s aa x' y' slot' slot. \<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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; \<forall>x y. c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; x' = fst slot; aa = DeleteDerived; y' = fst slot'; c slot' = Some slot\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag
 7. \<And>s aa x' y' ptr' uu_ uv_ auth ptr. \<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; \<forall>x y. c x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; \<forall>x y. c x = Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag; x' = ptr; aa = auth; y' = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag proof (prove)
goal:
No subgoals!