theory ArchVSpaceEntries_AI

lemma store_pte_non_master_valid_pdpt:
  "\<lbrace>valid_pdpt_objs and
        (\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) (p && ~~ mask pt_bits) s
        \<longrightarrow> (pte_range_sz (pt (ucast (p && mask pt_bits >> 2) && ~~ mask 4)) = 0
        \<and> pte_range_sz pte = 0))\<rbrace>
       store_pte p pte \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (simp add: store_pte_def set_pt_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 (case_tac "pt pa") apply simp apply (case_tac pte,simp_all) apply clarsimp apply (case_tac pte,simp_all) apply (simp add:fun_upd_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 (\<lambda>s. \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0 \<and> pte_range_sz pte = 0)\<rbrace> store_pte p pte \<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>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0 \<and> pte_range_sz pte = 0)) s \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) (p && ~~ 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) (p && mask pt_bits >> 2) := pte)))))) s proof (prove)
goal (1 subgoal):
 1. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> valid_entries pte_range (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) \<and> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> valid_entries pte_range (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))
 2. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> valid_entries pte_range pt
 2. \<And>s pt pa. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) \<inter> pte_range (pt pa) pa = {}
 3. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>s pt pa. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) \<inter> pte_range (pt pa) pa = {}
 2. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>s pt pa. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> ?x22 s pt pa \<in> ran (kheap s)
 2. \<And>s pt pa. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); obj_valid_pdpt (?x22 s pt pa)\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) \<inter> pte_range (pt pa) pa = {}
 3. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>s pt pa. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); obj_valid_pdpt (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) \<inter> pte_range (pt pa) pa = {}
 2. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (4 subgoals):
 1. \<And>s pt pa. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); obj_valid_pdpt (ArchObj (PageTable pt)); pt pa = InvalidPTE\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) \<inter> pte_range (pt pa) pa = {}
 2. \<And>s pt pa x21 x22 x23. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); obj_valid_pdpt (ArchObj (PageTable pt)); pt pa = LargePagePTE x21 x22 x23\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) \<inter> pte_range (pt pa) pa = {}
 3. \<And>s pt pa x31 x32 x33. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); obj_valid_pdpt (ArchObj (PageTable pt)); pt pa = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) \<inter> pte_range (pt pa) pa = {}
 4. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>s pt pa x21 x22 x23. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); obj_valid_pdpt (ArchObj (PageTable pt)); pt pa = LargePagePTE x21 x22 x23\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) \<inter> pte_range (pt pa) pa = {}
 2. \<And>s pt pa x31 x32 x33. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); obj_valid_pdpt (ArchObj (PageTable pt)); pt pa = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> pte_range pte (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) \<inter> pte_range (pt pa) pa = {}
 3. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (3 subgoals):
 1. \<And>s pt pa x21 x22 x23 x31 x32 x33. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pt \<and> entries_align pte_range_sz pt; pt pa = LargePagePTE x21 x22 x23; pte = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> is_aligned pa 4 \<longrightarrow> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4 \<noteq> pa
 2. \<And>s pt pa x31 x32 x33. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pt \<and> entries_align pte_range_sz pt; pt pa = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> pa \<notin> pte_range pte (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))
 3. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (2 subgoals):
 1. \<And>s pt pa x31 x32 x33. \<lbrakk>kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0; pa \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_entries pte_range pt \<and> entries_align pte_range_sz pt; pt pa = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> pa \<notin> pte_range pte (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))
 2. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (1 subgoal):
 1. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) proof (prove)
goal (1 subgoal):
 1. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (\<lambda>x. if x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) then pte else pt x) proof (prove)
goal (2 subgoals):
 1. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> entries_align pte_range_sz pt
 2. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> \<forall>x. x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> is_aligned x (pte_range_sz pte) proof (prove)
goal (1 subgoal):
 1. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) && ~~ mask 4)) = 0; pte_range_sz pte = 0\<rbrakk> \<Longrightarrow> \<forall>x. x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> is_aligned x (pte_range_sz pte) proof (prove)
goal:
No subgoals!