theory ArchCNode_AC

lemma store_pte_pas_refined[wp]:
  "\<lbrace>pas_refined aag and
    K (\<forall>x. pte_ref pte = Some x
           \<longrightarrow> (\<forall>a \<in> snd (snd x). \<forall>p' \<in> (ptr_range (fst x) (fst (snd x))).
                auth_graph_map (pasObjectAbs aag) {(p && ~~ mask pt_bits, a, p')} \<subseteq> pasPolicy aag))\<rbrace>
   store_pte p pte
   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" apply (simp add: auth_graph_map_def2) 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 split del: if_split) apply (erule state_bits_to_policy.cases,
          auto intro: state_bits_to_policy.intros auth_graph_map_memI
               split: if_split_asm)[1] apply (erule_tac B="state_asids_to_policy_aux _ _ _ _" in subset_trans[rotated]) apply (auto intro: state_asids_to_policy_aux.intros
              elim!: state_asids_to_policy_aux.cases
               elim: subset_trans[rotated]
              split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p'\<in>ptr_range (fst x) (fst (snd x)). auth_graph_map (pasObjectAbs aag) {(p && ~~ mask pt_bits, a, p')} \<subseteq> pasPolicy aag))\<rbrace> store_pte p pte \<lbrace>\<lambda>rv. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and (\<lambda>y. \<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pt_bits), ab, pasObjectAbs aag p') \<in> pasPolicy aag))\<rbrace> store_pte p pte \<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>y. \<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pt_bits), ab, pasObjectAbs aag p') \<in> pasPolicy aag))\<rbrace> store_pte p pte \<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>?Q22\<rbrace> store_pte p pte \<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>y. \<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pt_bits), ab, pasObjectAbs aag p') \<in> pasPolicy aag))) s \<Longrightarrow> ?Q22 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>y. \<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pt_bits), ab, pasObjectAbs aag p') \<in> pasPolicy aag))) s \<Longrightarrow> pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> (\<forall>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)(p && ~~ mask pt_bits := state_vrefs s (p && ~~ mask pt_bits) - S \<union> (\<Union>(p', sz, auth)\<in>set_option (pte_ref pte). (\<lambda>(p'', a). (p'', p && mask pt_bits >> 2, APageTable, a)) ` (ptr_range p' sz \<times> auth))))) \<subseteq> pasPolicy aag \<and> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) ((state_vrefs s)(p && ~~ mask pt_bits := state_vrefs s (p && ~~ mask pt_bits) - S \<union> (\<Union>(p', sz, auth)\<in>set_option (pte_ref pte). (\<lambda>(p'', a). (p'', p && mask pt_bits >> 2, APageTable, a)) ` (ptr_range p' sz \<times> auth)))) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s 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>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pt_bits), ab, pasObjectAbs aag p') \<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 && ~~ mask pt_bits then state_vrefs s (p && ~~ mask pt_bits) - S \<union> (\<Union>x\<in>set_option (pte_ref pte). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pt_bits >> 2, APageTable, a)) ` (ptr_range p' sz \<times> auth)) 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 && ~~ mask pt_bits then state_vrefs s (p && ~~ mask pt_bits) - S \<union> (\<Union>x\<in>set_option (pte_ref pte). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pt_bits >> 2, APageTable, a)) ` (ptr_range p' sz \<times> auth)) else state_vrefs s a) \<subseteq> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s 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>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pt_bits), ab, pasObjectAbs aag p') \<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 && ~~ mask pt_bits then state_vrefs s (p && ~~ mask pt_bits) - S \<union> (\<Union>x\<in>set_option (pte_ref pte). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pt_bits >> 2, APageTable, a)) ` (ptr_range p' sz \<times> auth)) else state_vrefs s a)) \<subseteq> pasPolicy aag
 2. \<And>s 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>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pt_bits), ab, pasObjectAbs aag p') \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (\<lambda>a. if a = p && ~~ mask pt_bits then state_vrefs s (p && ~~ mask pt_bits) - S \<union> (\<Union>x\<in>set_option (pte_ref pte). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pt_bits >> 2, APageTable, a)) ` (ptr_range p' sz \<times> auth)) else state_vrefs s a) \<subseteq> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s 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>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pt_bits), ab, pasObjectAbs aag p') \<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 && ~~ mask pt_bits then state_vrefs s (p && ~~ mask pt_bits) - S \<union> (\<Union>x\<in>set_option (pte_ref pte). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pt_bits >> 2, APageTable, a)) ` (ptr_range p' sz \<times> auth)) else state_vrefs s a)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x', aa, pasObjectAbs aag y') \<in> pasPolicy aag
 2. \<And>s 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>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pt_bits), ab, pasObjectAbs aag p') \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (\<lambda>a. if a = p && ~~ mask pt_bits then state_vrefs s (p && ~~ mask pt_bits) - S \<union> (\<Union>x\<in>set_option (pte_ref pte). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pt_bits >> 2, APageTable, a)) ` (ptr_range p' sz \<times> auth)) else state_vrefs s a) \<subseteq> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s 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>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pt_bits), ab, pasObjectAbs aag p') \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (\<lambda>a. if a = p && ~~ mask pt_bits then state_vrefs s (p && ~~ mask pt_bits) - S \<union> (\<Union>x\<in>set_option (pte_ref pte). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pt_bits >> 2, APageTable, a)) ` (ptr_range p' sz \<times> auth)) else state_vrefs s a) \<subseteq> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s 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_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<forall>a aa b. pte_ref pte = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pt_bits), ab, pasObjectAbs aag p') \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (\<lambda>a. if a = p && ~~ mask pt_bits then state_vrefs s (p && ~~ mask pt_bits) - S \<union> (\<Union>x\<in>set_option (pte_ref pte). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pt_bits >> 2, APageTable, a)) ` (ptr_range p' sz \<times> auth)) else state_vrefs s a) \<subseteq> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) proof (prove)
goal:
No subgoals!