theory ArchVSpaceEntries_AI

lemma mapM_x_store_pte_valid_pdpt2:
  "\<lbrace>valid_pdpt_objs and K (is_aligned ptr pt_bits)\<rbrace>
     mapM_x (\<lambda>x. store_pte x InvalidPTE) [ptr, ptr + 4 .e. ptr + 2 ^ pt_bits - 1]
   \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>" apply (rule hoare_gen_asm)+ apply (rule mapM_x_wp') apply (simp add:store_pte_def set_pt_def) apply (wp get_pt_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_pte_update) apply (drule (1) valid_pdpt_objs_ptD,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 ptr pt_bits)\<rbrace> mapM_x (\<lambda>x. store_pte x InvalidPTE) [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1] \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned ptr pt_bits \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> mapM_x (\<lambda>x. store_pte x InvalidPTE) [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1] \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> store_pte x InvalidPTE \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> do pt <- get_pt (x && ~~ mask pt_bits);
set_object (x && ~~ mask pt_bits) (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := InvalidPTE))))
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrakk> \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) (x && ~~ mask pt_bits) s \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and K (obj_valid_pdpt (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := InvalidPTE)))))) s proof (prove)
goal (1 subgoal):
 1. \<And>x s pt. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageTable pt) (x && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> valid_entries pte_range (pt(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := InvalidPTE)) \<and> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := InvalidPTE)) proof (prove)
goal (2 subgoals):
 1. \<And>x s pt. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageTable pt) (x && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> valid_entries pte_range (pt(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := InvalidPTE))
 2. \<And>x s pt. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageTable pt) (x && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := InvalidPTE)) proof (prove)
goal (3 subgoals):
 1. \<And>x s pt. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageTable pt) (x && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> valid_entries pte_range pt
 2. \<And>x s pt p. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageTable pt) (x && ~~ mask pt_bits) s; p \<noteq> UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> pte_range InvalidPTE (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) \<inter> pte_range (pt p) p = {}
 3. \<And>x s pt. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageTable pt) (x && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := InvalidPTE)) proof (prove)
goal (2 subgoals):
 1. \<And>x s pt p. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageTable pt) (x && ~~ mask pt_bits) s; p \<noteq> UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> pte_range InvalidPTE (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) \<inter> pte_range (pt p) p = {}
 2. \<And>x s pt. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageTable pt) (x && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := InvalidPTE)) proof (prove)
goal (1 subgoal):
 1. \<And>x s pt. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ako_at (PageTable pt) (x && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := InvalidPTE)) proof (prove)
goal (1 subgoal):
 1. \<And>x s pt. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (x && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (\<lambda>xa. if xa = UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) then InvalidPTE else pt xa) proof (prove)
goal (2 subgoals):
 1. \<And>x s pt. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (x && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz pt
 2. \<And>x s pt. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (x && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> \<forall>xa. xa = UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) \<longrightarrow> is_aligned xa (pte_range_sz InvalidPTE) proof (prove)
goal (1 subgoal):
 1. \<And>x s pt. \<lbrakk>is_aligned ptr pt_bits; x \<in> set [ptr , ptr + 4 .e. ptr + 2 ^ pt_bits - 1]; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (x && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> \<forall>xa. xa = UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) \<longrightarrow> is_aligned xa (pte_range_sz InvalidPTE) proof (prove)
goal:
No subgoals!