theory Finalise_AC

lemma thread_set_pas_refined_triv_idleT:
  assumes cps: "\<And>tcb. \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (f tcb) = getF tcb"
  and st: "\<And>tcb. P (tcb_state tcb) \<longrightarrow> tcb_state (f tcb) = tcb_state tcb"
  and ba: "\<And>tcb. Q (tcb_bound_notification tcb)
                  \<longrightarrow> tcb_bound_notification (f tcb) = tcb_bound_notification tcb"
  shows "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
                          and idle_tcb_at (\<lambda>(st, ntfn, arch). P st \<and> Q ntfn \<and> R arch) t\<rbrace>
         thread_set f t
         \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: pas_refined_def state_objs_to_policy_def) apply (rule hoare_pre) apply (wps thread_set_caps_of_state_trivial[OF cps]) apply (simp add: thread_set_def) apply (wpsimp wp: set_object_wp) apply (clarsimp simp: pred_tcb_def2 fun_upd_def[symmetric]
                   del: subsetI) apply (subst state_vrefs_tcb_upd, fastforce+) apply (clarsimp simp: tcb_at_def) apply (subst state_vrefs_tcb_upd, fastforce+) apply (clarsimp simp: tcb_at_def) apply (rule conjI) apply (erule_tac P="\<lambda> ts ba. auth_graph_map a (state_bits_to_policy cps ts ba cd vr) \<subseteq> ag"
                for a cps cd vr ag in rsubst') apply (drule get_tcb_SomeD) apply (rule ext, clarsimp simp add: thread_st_auth_def get_tcb_def st tcb_states_of_state_def) apply (drule get_tcb_SomeD) apply (rule ext, clarsimp simp: thread_bound_ntfns_def get_tcb_def ba) apply (clarsimp) 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 idle_tcb_at (\<lambda>(st, ntfn, arch). P st \<and> Q ntfn \<and> R arch) t\<rbrace> thread_set f t \<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 idle_tcb_at (\<lambda>(st, ab). P st \<and> (case ab of (ntfn, arch) \<Rightarrow> Q ntfn \<and> R arch)) t\<rbrace> thread_set f t \<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> thread_set f t \<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 idle_tcb_at (\<lambda>(st, ab). P st \<and> (case ab of (ntfn, arch) \<Rightarrow> Q ntfn \<and> R arch)) t) s \<Longrightarrow> ?Q6 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P9 prev_s\<rbrace> thread_set f t \<lbrace>\<lambda>rv s'. pas_wellformed aag \<and> irq_map_wellformed aag prev_s \<and> tcb_domain_map_wellformed aag prev_s \<and> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state prev_s) (thread_st_auth s') (thread_bound_ntfns s') (cdt prev_s) (state_vrefs s')) \<subseteq> pasPolicy aag \<and> state_asids_to_policy_arch aag (caps_of_state prev_s) (arch_state prev_s) (state_vrefs s') \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag prev_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 idle_tcb_at (\<lambda>(st, ab). P st \<and> (case ab of (ntfn, arch) \<Rightarrow> Q ntfn \<and> R arch)) t) s \<Longrightarrow> ?P9 s s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P9 prev_s\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>rv s'. pas_wellformed aag \<and> irq_map_wellformed aag prev_s \<and> tcb_domain_map_wellformed aag prev_s \<and> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state prev_s) (thread_st_auth s') (thread_bound_ntfns s') (cdt prev_s) (state_vrefs s')) \<subseteq> pasPolicy aag \<and> state_asids_to_policy_arch aag (caps_of_state prev_s) (arch_state prev_s) (state_vrefs s') \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag prev_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 idle_tcb_at (\<lambda>(st, ab). P st \<and> (case ab of (ntfn, arch) \<Rightarrow> Q ntfn \<and> R arch)) t) s \<Longrightarrow> ?P9 s 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 idle_tcb_at (\<lambda>(st, ab). P st \<and> (case ab of (ntfn, arch) \<Rightarrow> Q ntfn \<and> R arch)) t) s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> 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\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f (the (get_tcb t s))))\<rparr>)) (thread_bound_ntfns (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f (the (get_tcb t s))))\<rparr>)) (cdt s) (state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f (the (get_tcb t s))))\<rparr>))) \<subseteq> pasPolicy aag \<and> state_asids_to_policy_arch aag (caps_of_state s) (arch_state s) (state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f (the (get_tcb t s))))\<rparr>)) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) (thread_bound_ntfns (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) (cdt s) (state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>))) \<subseteq> pasPolicy aag \<and> state_asids_to_policy_arch aag (caps_of_state s) (arch_state s) (state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) \<subseteq> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s tcb. \<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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> tcb_at t s
 2. \<And>s tcb. \<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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) (thread_bound_ntfns (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag \<and> state_asids_to_policy_arch aag (caps_of_state s) (arch_state s) (state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) \<subseteq> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) (thread_bound_ntfns (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag \<and> state_asids_to_policy_arch aag (caps_of_state s) (arch_state s) (state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) \<subseteq> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s tcb. \<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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> tcb_at t s
 2. \<And>s tcb. \<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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) (thread_bound_ntfns (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) (thread_bound_ntfns (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s tcb. \<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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) (thread_bound_ntfns (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag
 2. \<And>s tcb. \<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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> state_asids_to_policy aag s \<subseteq> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>s tcb. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; 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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> thread_st_auth s = thread_st_auth (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)
 2. \<And>s tcb. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; 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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> thread_bound_ntfns s = thread_bound_ntfns (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)
 3. \<And>s tcb. \<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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> state_asids_to_policy aag s \<subseteq> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>s tcb. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; 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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> thread_st_auth s = thread_st_auth (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)
 2. \<And>s tcb. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; 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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> thread_bound_ntfns s = thread_bound_ntfns (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)
 3. \<And>s tcb. \<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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> state_asids_to_policy aag s \<subseteq> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s tcb. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; 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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> thread_bound_ntfns s = thread_bound_ntfns (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)
 2. \<And>s tcb. \<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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> state_asids_to_policy aag s \<subseteq> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s tcb. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; 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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> thread_bound_ntfns s = thread_bound_ntfns (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)
 2. \<And>s tcb. \<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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> state_asids_to_policy aag s \<subseteq> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<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; P (tcb_state tcb); Q (tcb_bound_notification tcb); R (tcb_iarch tcb); get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> state_asids_to_policy aag s \<subseteq> pasPolicy aag proof (prove)
goal:
No subgoals!