theory ArchFinalise_IF

lemma mapM_x_swp_store_kernel_base_globals_equiv:
  "\<lbrace>invs and globals_equiv st and cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap word option))) slot\<rbrace>
   mapM_x (swp store_pde InvalidPDE) (map ((\<lambda>x. x + word) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1])
   \<lbrace>\<lambda>_ s. globals_equiv st s \<and> invs s\<rbrace>" apply (rule hoare_pre) apply (wp mapM_x_swp_store_pde_invs_unmap mapM_x_swp_store_pde_globals_equiv) apply clarsimp apply (frule invs_valid_objs) apply (frule invs_valid_global_refs) apply (intro impI conjI allI) by (simp add: cte_wp_at_page_directory_not_in_globals
                cte_wp_at_page_directory_not_in_kernel_mappings
                not_in_global_not_arm pde_ref_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and globals_equiv st and cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap word option))) slot\<rbrace> mapM_x (swp store_pde InvalidPDE) (map ((\<lambda>x. x + word) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]) \<lbrace>\<lambda>_ s. globals_equiv st s \<and> invs s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> mapM_x (swp store_pde InvalidPDE) (map ((\<lambda>x. x + word) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]) \<lbrace>\<lambda>_ s. globals_equiv st s \<and> invs s\<rbrace>
 2. \<And>s. (invs and globals_equiv st and cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap word option))) slot) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and globals_equiv st and cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap word option))) slot) s \<Longrightarrow> (globals_equiv st and (\<lambda>s. \<forall>x\<in>set (map ((\<lambda>x. x + word) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]). x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))) s \<and> (invs and K (\<forall>sl\<in>set (map ((\<lambda>x. x + word) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]). UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set (map ((\<lambda>x. x + word) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]). sl && ~~ mask pd_bits \<notin> global_refs s) and K (InvalidPDE = InvalidPDE)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; globals_equiv st s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap word option))) slot s\<rbrakk> \<Longrightarrow> (\<forall>x\<le>(kernel_base >> 20) - 1. (x << 2) + word && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)) \<and> (\<forall>sl\<le>(kernel_base >> 20) - 1. UCAST(32 \<rightarrow> 12) ((sl << 2) + word && mask pd_bits >> 2) \<notin> kernel_mapping_slots) \<and> (\<forall>sl\<le>(kernel_base >> 20) - 1. (sl << 2) + word && ~~ mask pd_bits \<notin> global_refs s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; globals_equiv st s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap word option))) slot s; valid_objs s\<rbrakk> \<Longrightarrow> (\<forall>x\<le>(kernel_base >> 20) - 1. (x << 2) + word && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)) \<and> (\<forall>sl\<le>(kernel_base >> 20) - 1. UCAST(32 \<rightarrow> 12) ((sl << 2) + word && mask pd_bits >> 2) \<notin> kernel_mapping_slots) \<and> (\<forall>sl\<le>(kernel_base >> 20) - 1. (sl << 2) + word && ~~ mask pd_bits \<notin> global_refs s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; globals_equiv st s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap word option))) slot s; valid_objs s; valid_global_refs s\<rbrakk> \<Longrightarrow> (\<forall>x\<le>(kernel_base >> 20) - 1. (x << 2) + word && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)) \<and> (\<forall>sl\<le>(kernel_base >> 20) - 1. UCAST(32 \<rightarrow> 12) ((sl << 2) + word && mask pd_bits >> 2) \<notin> kernel_mapping_slots) \<and> (\<forall>sl\<le>(kernel_base >> 20) - 1. (sl << 2) + word && ~~ mask pd_bits \<notin> global_refs s) proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>invs s; globals_equiv st s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap word option))) slot s; valid_objs s; valid_global_refs s; x \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> (x << 2) + word && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)
 2. \<And>s sl. \<lbrakk>invs s; globals_equiv st s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap word option))) slot s; valid_objs s; valid_global_refs s; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((sl << 2) + word && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 3. \<And>s sl. \<lbrakk>invs s; globals_equiv st s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap word option))) slot s; valid_objs s; valid_global_refs s; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> (sl << 2) + word && ~~ mask pd_bits \<notin> global_refs s