theory Finalise_AC

lemma sbn_pas_refined[wp]:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and
    K (case ntfn of None \<Rightarrow> True
                  | Some ntfn' \<Rightarrow> \<forall>auth \<in> {Receive, Reset}. abs_has_auth_to aag auth t ntfn')\<rbrace>
   set_bound_notification t ntfn
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: pas_refined_def state_objs_to_policy_def) apply (rule hoare_pre) apply (wp tcb_domain_map_wellformed_lift sbn_st_vrefs | wps)+ apply (clarsimp dest!: auth_graph_map_memD) apply (erule state_bits_to_policy.cases) by (auto intro: state_bits_to_policy.intros auth_graph_map_memI
           split: if_split_asm)

(* 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 K (case ntfn of None \<Rightarrow> True | Some ntfn' \<Rightarrow> \<forall>auth\<in>{Receive, Reset}. (pasObjectAbs aag t, auth, pasObjectAbs aag ntfn') \<in> pasPolicy aag)\<rbrace> set_bound_notification t ntfn \<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>y. case ntfn of None \<Rightarrow> True | Some ntfn' \<Rightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfn') \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Reset, pasObjectAbs aag ntfn') \<in> pasPolicy aag)\<rbrace> set_bound_notification t ntfn \<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>?Q11\<rbrace> set_bound_notification t ntfn \<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>y. case ntfn of None \<Rightarrow> True | Some ntfn' \<Rightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfn') \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Reset, pasObjectAbs aag ntfn') \<in> pasPolicy aag)) s \<Longrightarrow> ?Q11 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>y. case ntfn of None \<Rightarrow> True | Some ntfn' \<Rightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfn') \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Reset, pasObjectAbs aag ntfn') \<in> pasPolicy aag)) s \<Longrightarrow> ((\<lambda>s. pas_wellformed aag) and pspace_aligned and valid_vspace_objs and valid_arch_state) s \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> ((\<lambda>sa. auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) ((thread_bound_ntfns s)(t := ntfn)) (cdt s) (state_vrefs sa)) \<subseteq> pasPolicy aag \<and> state_asids_to_policy_arch aag (caps_of_state s) (arch_state s) (state_vrefs sa) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag) and pspace_aligned and valid_vspace_objs and valid_arch_state) s 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) (\<lambda>a. if a = t then ntfn else thread_bound_ntfns s a) (cdt s) (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; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; case ntfn of None \<Rightarrow> True | Some ntfn' \<Rightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfn') \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Reset, pasObjectAbs aag ntfn') \<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; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; case ntfn of None \<Rightarrow> True | Some ntfn' \<Rightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfn') \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Reset, pasObjectAbs aag ntfn') \<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; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; case ntfn of None \<Rightarrow> True | Some ntfn' \<Rightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfn') \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Reset, pasObjectAbs aag ntfn') \<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; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; case ntfn of None \<Rightarrow> True | Some ntfn' \<Rightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfn') \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Reset, pasObjectAbs aag ntfn') \<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; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; case ntfn of None \<Rightarrow> True | Some ntfn' \<Rightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfn') \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Reset, pasObjectAbs aag ntfn') \<in> pasPolicy aag; x' = oref; aa = auth; y' = oref'; (if oref = t then ntfn else 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; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; case ntfn of None \<Rightarrow> True | Some ntfn' \<Rightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfn') \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Reset, pasObjectAbs aag ntfn') \<in> pasPolicy aag; x' = fst slot; aa = Control; y' = fst slot'; cdt s 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; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; case ntfn of None \<Rightarrow> True | Some ntfn' \<Rightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfn') \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Reset, pasObjectAbs aag ntfn') \<in> pasPolicy aag; x' = fst slot; aa = DeleteDerived; y' = fst slot'; cdt s 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; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; case ntfn of None \<Rightarrow> True | Some ntfn' \<Rightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfn') \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Reset, pasObjectAbs aag ntfn') \<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