theory ArchVSpaceEntries_AI

lemma mapM_x_store_pde_valid_pdpt2:
  "\<lbrace>valid_pdpt_objs and K (is_aligned pd pd_bits)\<rbrace>
       mapM_x (\<lambda>x. store_pde ((x << 2) + pd) pde.InvalidPDE)
        [0.e.(kernel_base >> 20) - 1]
       \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (rule hoare_gen_asm) apply (rule mapM_x_wp') apply (simp add:store_pde_def set_pd_def) apply (wp get_pd_wp get_object_wp) apply (clarsimp simp: mask_in_range
    split:Structures_A.kernel_object.splits
    arch_kernel_obj.splits) apply (rule conjI) apply (rule valid_entries_overwrite_0) apply (fastforce simp:ran_def obj_at_def) apply simp apply (simp add:fun_upd_def obj_at_def) apply (rule entries_align_pde_update) apply (drule (1) valid_pdpt_objs_pdD,simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and K (is_aligned pd pd_bits)\<rbrace> mapM_x (\<lambda>x. store_pde ((x << 2) + pd) InvalidPDE) [0 .e. (kernel_base >> 20) - 1] \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> mapM_x (\<lambda>x. store_pde ((x << 2) + pd) InvalidPDE) [0 .e. (kernel_base >> 20) - 1] \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned pd pd_bits; x \<in> set [0 .e. (kernel_base >> 20) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> store_pde ((x << 2) + pd) InvalidPDE \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> do pda <- get_pd ((x << 2) + pd && ~~ mask pd_bits);
set_object ((x << 2) + pd && ~~ mask pd_bits) (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2) := InvalidPDE))))
od \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrakk> \<Longrightarrow> \<forall>pda. ako_at (PageDirectory pda) ((x << 2) + pd && ~~ mask pd_bits) s \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and K (obj_valid_pdpt (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2) := InvalidPDE)))))) s proof (prove)
goal (1 subgoal):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pda) ((x << 2) + pd && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> valid_entries pde_range (pda(UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2) := InvalidPDE)) \<and> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2) := InvalidPDE)) proof (prove)
goal (2 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pda) ((x << 2) + pd && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> valid_entries pde_range (pda(UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2) := InvalidPDE))
 2. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pda) ((x << 2) + pd && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2) := InvalidPDE)) proof (prove)
goal (3 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pda) ((x << 2) + pd && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> valid_entries pde_range pda
 2. \<And>x s pda p. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pda) ((x << 2) + pd && ~~ mask pd_bits) s; p \<noteq> UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> pde_range InvalidPDE (UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2)) \<inter> pde_range (pda p) p = {}
 3. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pda) ((x << 2) + pd && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2) := InvalidPDE)) proof (prove)
goal (2 subgoals):
 1. \<And>x s pda p. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pda) ((x << 2) + pd && ~~ mask pd_bits) s; p \<noteq> UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> pde_range InvalidPDE (UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2)) \<inter> pde_range (pda p) p = {}
 2. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pda) ((x << 2) + pd && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2) := InvalidPDE)) proof (prove)
goal (1 subgoal):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageDirectory pda) ((x << 2) + pd && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pda(UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2) := InvalidPDE)) proof (prove)
goal (1 subgoal):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s ((x << 2) + pd && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>xa. if xa = UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2) then InvalidPDE else pda xa) proof (prove)
goal (2 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s ((x << 2) + pd && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> entries_align pde_range_sz pda
 2. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s ((x << 2) + pd && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> \<forall>xa. xa = UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2) \<longrightarrow> is_aligned xa (pde_range_sz InvalidPDE) proof (prove)
goal (1 subgoal):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; x \<le> (kernel_base >> 20) - 1; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s ((x << 2) + pd && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> \<forall>xa. xa = UCAST(32 \<rightarrow> 12) ((x << 2) + pd && mask pd_bits >> 2) \<longrightarrow> is_aligned xa (pde_range_sz InvalidPDE) proof (prove)
goal:
No subgoals!