theory ArchVSpaceEntries_AI

lemma store_invalid_pte_valid_pdpt:
  "\<lbrace>valid_pdpt_objs and
        (\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) (p && ~~ mask pt_bits) s
        \<longrightarrow> pte = InvalidPTE)\<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, simp_all) apply (fastforce simp: ran_def) 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 = InvalidPTE)\<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. (\<exists>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s) \<longrightarrow> pte = InvalidPTE)) 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; pte = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> valid_entries pte_range (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)) \<and> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)) proof (prove)
goal (2 subgoals):
 1. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pte = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> valid_entries pte_range (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE))
 2. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pte = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)) proof (prove)
goal (2 subgoals):
 1. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pte = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> valid_entries pte_range pt
 2. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pte = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)) proof (prove)
goal (1 subgoal):
 1. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pte = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)) proof (prove)
goal (1 subgoal):
 1. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pte = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (\<lambda>x. if x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) then InvalidPTE else pt x) proof (prove)
goal (2 subgoals):
 1. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pte = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> entries_align pte_range_sz pt
 2. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pte = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> \<forall>x. x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> is_aligned x (pte_range_sz InvalidPTE) proof (prove)
goal (1 subgoal):
 1. \<And>s pt. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pte = InvalidPTE; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> \<forall>x. x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> is_aligned x (pte_range_sz InvalidPTE) proof (prove)
goal:
No subgoals!