theory Arch_AC

lemma as_user_pas_refined[wp]:
  "\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and pas_refined aag\<rbrace>
   as_user t f
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: pas_refined_def state_objs_to_policy_def) apply (rule hoare_pre) apply wps apply (wp as_user_state_vrefs) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and pas_refined aag\<rbrace> as_user t f \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<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> as_user t f \<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> as_user t f \<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. (pspace_aligned and valid_vspace_objs and valid_arch_state and (\<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)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P9 prev_s\<rbrace> as_user t f \<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 prev_s) (thread_bound_ntfns prev_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. (pspace_aligned and valid_vspace_objs and valid_arch_state and (\<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)) s \<Longrightarrow> ?P9 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned and valid_vspace_objs and valid_arch_state and (\<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)) s \<Longrightarrow> (pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>sa. 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 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:
No subgoals!