theory ArchCNode_AC

lemma store_pde_pas_refined[wp]:
  "\<lbrace>pas_refined aag and
    K ((ucast (p && mask pd_bits >> 2)::12 word) < (ucast (kernel_base >> 20))
       \<longrightarrow> (\<forall>x. pde_ref2 pde = 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 pd_bits, a, p')} \<subseteq> pasPolicy aag)))\<rbrace>
   store_pde p pde
   \<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 split del: if_split) 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
              split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>x. pde_ref2 pde = 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 pd_bits, a, p')} \<subseteq> pasPolicy aag)))\<rbrace> store_pde p pde \<lbrace>\<lambda>rv. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and (\<lambda>y. UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pd_bits), ab, pasObjectAbs aag p') \<in> pasPolicy aag)))\<rbrace> store_pde p pde \<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. UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pd_bits), ab, pasObjectAbs aag p') \<in> pasPolicy aag)))\<rbrace> store_pde p pde \<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>?Q24\<rbrace> store_pde p pde \<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. UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pd_bits), ab, pasObjectAbs aag p') \<in> pasPolicy aag)))) s \<Longrightarrow> ?Q24 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. UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pd_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 pd_bits := state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>(p', sz, auth)\<in>set_option (pde_ref2 pde). (\<lambda>(p'', a). (p'', p && mask pd_bits >> 2, APageDirectory, 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 pd_bits := state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>(p', sz, auth)\<in>set_option (pde_ref2 pde). (\<lambda>(p'', a). (p'', p && mask pd_bits >> 2, APageDirectory, 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; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pd_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 pd_bits then state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>x\<in>set_option (pde_ref2 pde). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pd_bits >> 2, APageDirectory, 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 pd_bits then state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>x\<in>set_option (pde_ref2 pde). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pd_bits >> 2, APageDirectory, 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; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pd_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 pd_bits then state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>x\<in>set_option (pde_ref2 pde). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pd_bits >> 2, APageDirectory, 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; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pd_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 pd_bits then state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>x\<in>set_option (pde_ref2 pde). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pd_bits >> 2, APageDirectory, 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; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pd_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 pd_bits then state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>x\<in>set_option (pde_ref2 pde). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pd_bits >> 2, APageDirectory, 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; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pd_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 pd_bits then state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>x\<in>set_option (pde_ref2 pde). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pd_bits >> 2, APageDirectory, 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; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pd_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 pd_bits then state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>x\<in>set_option (pde_ref2 pde). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pd_bits >> 2, APageDirectory, 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; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 pde = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. (pasObjectAbs aag (p && ~~ mask pd_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 pd_bits then state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>x\<in>set_option (pde_ref2 pde). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pd_bits >> 2, APageDirectory, 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!