theory ArchVSpace_AI

lemma mapM_swp_store_pde_invs_unmap:
  "\<lbrace>invs and
    (\<lambda>s. \<forall>sl\<in>set slots.
            ucast (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and
    (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and
    K (pde = InvalidPDE)\<rbrace>
  mapM (swp store_pde pde) slots \<lbrace>\<lambda>_. invs\<rbrace>" apply (rule hoare_post_imp) prefer 2 apply (rule mapM_wp') apply simp apply (rule hoare_pre, wp store_pde_invs_unmap hoare_vcg_const_Ball_lift
                             hoare_vcg_ex_lift) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<forall>sl\<in>set slots. UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and K (pde = InvalidPDE)\<rbrace> mapM (swp store_pde pde) slots \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. ?Q rv s \<Longrightarrow> invs s
 2. \<lbrace>invs and (\<lambda>s. \<forall>sl\<in>set slots. UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and K (pde = InvalidPDE)\<rbrace> mapM (swp store_pde pde) slots \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>invs and (\<lambda>s. \<forall>sl\<in>set slots. UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and K (pde = InvalidPDE)\<rbrace> mapM (swp store_pde pde) slots \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> invs s proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set slots \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<forall>sl\<in>set slots. UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and K (pde = InvalidPDE)\<rbrace> swp store_pde pde x \<lbrace>\<lambda>rv. invs and (\<lambda>s. \<forall>sl\<in>set slots. UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and K (pde = InvalidPDE)\<rbrace>
 2. \<And>rv s. (invs and (\<lambda>s. \<forall>sl\<in>set slots. UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and K (pde = InvalidPDE)) s \<Longrightarrow> invs s proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set slots \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<forall>sl\<in>set slots. UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and (\<lambda>y. pde = InvalidPDE)\<rbrace> store_pde x pde \<lbrace>\<lambda>rv. invs and (\<lambda>s. \<forall>sl\<in>set slots. UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and (\<lambda>y. pde = InvalidPDE)\<rbrace>
 2. \<And>rv s. (invs and (\<lambda>s. \<forall>sl\<in>set slots. UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and K (pde = InvalidPDE)) s \<Longrightarrow> invs s proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set slots; (invs and (\<lambda>s. \<forall>sl\<in>set slots. UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and (\<lambda>y. pde = InvalidPDE)) s\<rbrakk> \<Longrightarrow> (invs and valid_pde pde and (\<lambda>s. wellformed_pde pde) and K (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. x && ~~ mask pd_bits \<notin> global_refs s) and K (pde = InvalidPDE)) s \<and> (\<forall>x\<in>set slots. UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots) \<and> (\<forall>x\<in>set slots. x && ~~ mask pd_bits \<notin> global_refs s) \<and> pde = InvalidPDE
 2. \<And>rv s. (invs and (\<lambda>s. \<forall>sl\<in>set slots. UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and K (pde = InvalidPDE)) s \<Longrightarrow> invs s proof (prove)
goal:
No subgoals!