theory ArchVSpaceEntries_AI

lemma store_pde_non_master_valid_pdpt:
  "\<lbrace>valid_pdpt_objs and
        (\<lambda>s. \<forall>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s
        \<longrightarrow> (pde_range_sz (pd (ucast (p && mask pd_bits >> 2) && ~~ mask 4)) = 0
        \<and> pde_range_sz pde = 0))\<rbrace>
       store_pde p pde \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (simp add: store_pde_def set_pd_def, wp get_object_wp) apply (clarsimp simp: obj_at_def) apply (intro conjI) apply (rule valid_entries_overwrite_0) apply (fastforce simp:ran_def) apply (drule bspec) apply fastforce apply (rename_tac p') apply (case_tac "pd p'"; cases pde; clarsimp) apply (simp add:fun_upd_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 (\<lambda>s. \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0 \<and> pde_range_sz pde = 0)\<rbrace> store_pde p pde \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and (\<lambda>s. \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0 \<and> pde_range_sz pde = 0)) s \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and K (obj_valid_pdpt (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))))) s proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> valid_entries pde_range (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) \<and> entries_align pde_range_sz (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> valid_entries pde_range (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))
 2. \<And>s pd. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>s pd. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> valid_entries pde_range pd
 2. \<And>s pd pa. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0; pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> pde_range pde (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) \<inter> pde_range (pd pa) pa = {}
 3. \<And>s pd. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pa. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0; pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> pde_range pde (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) \<inter> pde_range (pd pa) pa = {}
 2. \<And>s pd. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>s pd pa. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0; pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> ?x22 s pd pa \<in> ran (kheap s)
 2. \<And>s pd pa. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0; pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); obj_valid_pdpt (?x22 s pd pa)\<rbrakk> \<Longrightarrow> pde_range pde (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) \<inter> pde_range (pd pa) pa = {}
 3. \<And>s pd. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>s pd pa. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0; pa \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); obj_valid_pdpt (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> pde_range pde (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) \<inter> pde_range (pd pa) pa = {}
 2. \<And>s pd. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>s pd p'. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0; p' \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); obj_valid_pdpt (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> pde_range pde (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) \<inter> pde_range (pd p') p' = {}
 2. \<And>s pd. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> entries_align pde_range_sz (\<lambda>x. if x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pd x) proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> entries_align pde_range_sz pd
 2. \<And>s pd. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> \<forall>x. x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> is_aligned x (pde_range_sz pde) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) && ~~ mask 4)) = 0; pde_range_sz pde = 0\<rbrakk> \<Longrightarrow> \<forall>x. x = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> is_aligned x (pde_range_sz pde) proof (prove)
goal:
No subgoals!