theory ArchVSpace_AI

lemma unmap_page_table_unmapped[wp]:
  "\<lbrace>pspace_aligned and valid_vspace_objs\<rbrace>
     unmap_page_table asid vaddr pt
   \<lbrace>\<lambda>rv s. \<not> ([VSRef (vaddr >> 20) (Some APageDirectory),
               VSRef (asid && mask asid_low_bits) (Some AASIDPool),
               VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pt) s\<rbrace>" apply (simp add: unmap_page_table_def lookup_pd_slot_def Let_def
             cong: option.case_cong) apply (rule hoare_pre) apply ((wp store_pde_unmap_pt page_table_mapped_wp | wpc | simp)+)[1] apply (clarsimp simp: vspace_at_asid_def pd_aligned pd_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> unmap_page_table asid vaddr pt \<lbrace>\<lambda>rv s. ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> do pdOpt <- page_table_mapped asid vaddr pt;
case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do y <- store_pde (pd + (vaddr >> 20 << 2)) InvalidPDE;
y <- do_machine_op (cleanByVA_PoU (pd + (vaddr >> 20 << 2)) (addrFromPPtr (pd + (vaddr >> 20 << 2))));
flush_table pd asid vaddr pt
od
od \<lbrace>\<lambda>rv s. ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> do pdOpt <- page_table_mapped asid vaddr pt;
case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do y <- store_pde (pd + (vaddr >> 20 << 2)) InvalidPDE;
y <- do_machine_op (cleanByVA_PoU (pd + (vaddr >> 20 << 2)) (addrFromPPtr (pd + (vaddr >> 20 << 2))));
flush_table pd asid vaddr pt
od
od \<lbrace>\<lambda>rv s. ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s\<rbrace>
 2. \<And>s. (pspace_aligned and valid_vspace_objs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned and valid_vspace_objs) s \<Longrightarrow> valid_vspace_objs s \<and> pspace_aligned s \<and> (([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> (None = None \<longrightarrow> ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s) \<and> (\<forall>x. None = Some x \<longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x and K (is_aligned x pd_bits)) s)) \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> (Some pd = None \<longrightarrow> ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s) \<and> (\<forall>x. Some pd = Some x \<longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x and K (is_aligned x pd_bits)) s)) proof (prove)
goal:
No subgoals!