theory ArchCNode_AC

lemma set_asid_pool_pas_refined[wp]:
  "\<lbrace>pas_refined aag and
    (\<lambda>s. \<forall>(x, y) \<in> graph_of pool.
           auth_graph_map (pasObjectAbs aag) {(p, Control, y)} \<subseteq> pasPolicy aag \<and>
           (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some p \<and>
                   asid && mask asid_low_bits = ucast x
                   \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag y) \<in> pasPolicy aag))\<rbrace>
         set_asid_pool p pool \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" apply (simp add: auth_graph_map_def2 image_UN split_def) 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 apply (rule conjI) 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)[1] apply (auto intro: state_asids_to_policy_aux.intros
               simp: subsetD[OF _ state_asids_to_policy_aux.intros(2)]
              elim!: state_asids_to_policy_aux.cases
              split: if_split_asm) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and (\<lambda>s. \<forall>(x, y)\<in>graph_of pool. auth_graph_map (pasObjectAbs aag) {(p, Control, y)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some p \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) x \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag y) \<in> pasPolicy aag))\<rbrace> set_asid_pool p pool \<lbrace>\<lambda>rv. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and (\<lambda>s. \<forall>x\<in>graph_of pool. (pasObjectAbs aag p, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some p \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) (fst x) \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag))\<rbrace> set_asid_pool p pool \<lbrace>\<lambda>rv. 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_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag) and (\<lambda>s. \<forall>x\<in>graph_of pool. (pasObjectAbs aag p, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some p \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) (fst x) \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag))\<rbrace> set_asid_pool p pool \<lbrace>\<lambda>rv 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_aux aag (caps_of_state s) (asid_table s) (state_vrefs 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_asid_pool p pool \<lbrace>\<lambda>rv 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_aux aag (caps_of_state s) (asid_table s) (state_vrefs 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_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag) and (\<lambda>s. \<forall>x\<in>graph_of pool. (pasObjectAbs aag p, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some p \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) (fst x) \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag (snd x)) \<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_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag) and (\<lambda>s. \<forall>x\<in>graph_of pool. (pasObjectAbs aag p, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some p \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) (fst x) \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag))) s \<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) (thread_bound_ntfns s) (cdt s) ((state_vrefs s)(p := (\<lambda>a. case a of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool))) \<subseteq> pasPolicy aag \<and> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) ((state_vrefs s)(p := (\<lambda>a. case a of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool)) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s. \<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_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<forall>x\<in>graph_of pool. (pasObjectAbs aag p, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some p \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) (fst x) \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (\<lambda>a. if a = p then (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool else state_vrefs s a)) \<subseteq> pasPolicy aag \<and> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (\<lambda>a. if a = p then (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool else state_vrefs s a) \<subseteq> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s. \<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_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<forall>x\<in>graph_of pool. (pasObjectAbs aag p, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some p \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) (fst x) \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (\<lambda>a. if a = p then (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool else state_vrefs s a)) \<subseteq> pasPolicy aag
 2. \<And>s. \<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_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<forall>x\<in>graph_of pool. (pasObjectAbs aag p, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some p \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) (fst x) \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (\<lambda>a. if a = p then (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool else state_vrefs s a) \<subseteq> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s aa x' y'. \<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_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<forall>x\<in>graph_of pool. (pasObjectAbs aag p, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some p \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) (fst x) \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag); (x', aa, y') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (\<lambda>a. if a = p then (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool else state_vrefs s a)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag
 2. \<And>s. \<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_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<forall>x\<in>graph_of pool. (pasObjectAbs aag p, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some p \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) (fst x) \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (\<lambda>a. if a = p then (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool else state_vrefs s a) \<subseteq> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s. \<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_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<forall>x\<in>graph_of pool. (pasObjectAbs aag p, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some p \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) (fst x) \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (\<lambda>a. if a = p then (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool else state_vrefs s a) \<subseteq> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s asid a b. \<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_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<forall>x\<in>graph_of pool. (pasObjectAbs aag p, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some p \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) (fst x) \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag (snd x)) \<in> pasPolicy aag); asid_table s (asid_high_bits_of asid) = Some p; (a, b) \<in> graph_of pool; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag b) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!