theory CNode_AC

lemma set_thread_state_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and
    K (\<forall>r \<in> tcb_st_to_auth st. abs_has_auth_to aag (snd r) t (fst r))\<rbrace>
   set_thread_state t st
   \<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 | wps)+ apply (clarsimp dest!: auth_graph_map_memD) apply (erule state_bits_to_policy.cases;
         auto intro: state_bits_to_policy.intros auth_graph_map_memI
              split: if_split_asm) 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 K (\<forall>r\<in>tcb_st_to_auth st. (pasObjectAbs aag t, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)\<rbrace> set_thread_state t st \<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. \<forall>r\<in>tcb_st_to_auth st. (pasObjectAbs aag t, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)\<rbrace> set_thread_state t st \<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_thread_state t st \<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. \<forall>r\<in>tcb_st_to_auth st. (pasObjectAbs aag t, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) 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>y. \<forall>r\<in>tcb_st_to_auth st. (pasObjectAbs aag t, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<Longrightarrow> (pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. pas_wellformed aag)) s \<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) ((thread_st_auth s)(t := tcb_st_to_auth st)) (thread_bound_ntfns s) (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)) 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) (\<lambda>a. if a = t then tcb_st_to_auth st else thread_st_auth s a) (thread_bound_ntfns s) (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; \<forall>r\<in>tcb_st_to_auth st. (pasObjectAbs aag t, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag proof (prove)
goal:
No subgoals!