theory ArchVSpaceEntries_AI

lemma unmap_page_table_valid_pdpt_objs[wp]:
  notes hoare_pre [wp_pre del]
  shows "\<lbrace>valid_pdpt_objs\<rbrace> unmap_page_table asid vptr pt \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (simp add: unmap_page_table_def) apply (wp get_object_wp store_invalid_pde_valid_pdpt | wpc)+ apply (simp add: obj_at_def) apply (simp add: page_table_mapped_def) apply (wp get_pde_wp | wpc)+ apply simp apply (rule hoare_post_impErr, rule valid_validE,
         rule find_pd_for_asid_inv, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> unmap_page_table asid vptr pt \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> do pdOpt <- page_table_mapped asid vptr pt;
case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do y <- store_pde (lookup_pd_slot pd vptr) InvalidPDE;
y <- do_machine_op (cleanByVA_PoU (lookup_pd_slot pd vptr) (addrFromPPtr (lookup_pd_slot pd vptr)));
flush_table pd asid vptr pt
od
od \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt s. (pdOpt = None \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>x. pdOpt = Some x \<longrightarrow> ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and (\<lambda>s. \<forall>pd. ako_at (PageDirectory pd) (lookup_pd_slot x vptr && ~~ mask pd_bits) s \<longrightarrow> InvalidPDE = InvalidPDE)) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt s. Ball (ran (kheap s)) obj_valid_pdpt\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vptr)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE <catch> (\<lambda>y. return None) \<lbrace>\<lambda>pdOpt s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd s. \<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>x xa xb xc. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SectionPDE x xa xb xc \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> (\<forall>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SuperSectionPDE x xa xb \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x))\<rbrace>, \<lbrace>\<lambda>x a. \<forall>x\<in>ran (kheap a). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd s. \<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> ((\<exists>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> ((\<exists>x xa xb xc. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SectionPDE x xa xb xc) \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) \<and> ((\<exists>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SuperSectionPDE x xa xb) \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x))\<rbrace>, \<lbrace>\<lambda>x a. \<forall>x\<in>ran (kheap a). obj_valid_pdpt x\<rbrace> proof (prove)
goal:
No subgoals!